Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard max-plus'' and min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.
Recently, Sharma @cite_7 proposed a machine-learning based approach to find disjunctive invariants. Their method operates on traces representing good and bad program states: good traces are obtained by running the program on random inputs and bad traces correspond to runs on which an assertion or postcondition is violated. They use a machine learning model to find a predicate, representing a candidate program invariant, that separates the good and bad traces. For efficiency, they restrict attention to the octagon domain and search only for predicates that are arbitrary boolean combinations of octagon inequalities. Finally, they use standard induction technique to check the candidate invariants using Z3 @cite_41 . While our method shares their focus on disjunctive invariants, a key difference is that the strength of their results depends strictly on existing annotated program assertions. For example, in ex1 , if the line assert(y==11) is not provided by the programmer then their method will only produce the trivial invariant @math . By contrast, our approach does not make such assumptions about the input program, and in some sense the purpose of our approach is to generate those assertions.
@cite_41 @cite_7
1480909796 2280703106
Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications. We formalize the problem of program verification as a learning problem, showing that invariants in program verification can be regarded as geometric concepts in machine learning. Safety properties define bad states: states a program should not reach. Program verification explains why a program’s set of reachable states is disjoint from the set of bad states. In Hoare Logic, these explanations are predicates that form inductive assertions. Using samples for reachable and bad states and by applying well known machine learning algorithms for classification, we are able to generate inductive assertions. By relaxing the search for an exact proof to classifiers, we obtain complexity theoretic improvements. Further, we extend the learning algorithm to obtain a sound procedure that can generate proofs containing invariants that are arbitrary boolean combinations of polynomial inequalities. We have evaluated our approach on a number of challenging benchmarks and the results are promising.