A Survey of Satisfiability Modulo Theory <s> Craig Interpolation <s> We present a method of deriving Craig interpolants from proofs in the quantifier-free theory of linear inequality and uninterpreted function symbols, and an interpolating theorem prover based on this method. The prover has been used for predicate refinement in the BLAST software model checker, and can also be used directly for model checking infinite-state systems, using interpolation-based image approximation. <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> Craig Interpolation <s> We describe a model checker for infinite-state sequential programs, based on Craig interpolation and the lazy abstraction paradigm. On device driver benchmarks, we observe a speedup of up to two orders of magnitude relative to a similar tool using predicate abstraction. <s> BIB002 </s> A Survey of Satisfiability Modulo Theory <s> Craig Interpolation <s> We show how interpolants can be viewed as classifiers in supervised machine learning. This view has several advantages: First, we are able to use off-the-shelf classification techniques, in particular support vector machines (SVMs), for interpolation. Second, we show that SVMs can find relevant predicates for a number of benchmarks. Since classification algorithms are predictive, the interpolants computed via classification are likely to be invariants. Finally, the machine learning view also enables us to handle superficial non-linearities. Even if the underlying problem structure is linear, the symbolic constraints can give an impression that we are solving a non-linear problem. Since learning algorithms try to mine the underlying structure directly, we can discover the linear structure for such problems. We demonstrate the feasibility of our approach via experiments over benchmarks from various papers on program verification. <s> BIB003 </s> A Survey of Satisfiability Modulo Theory <s> Craig Interpolation <s> Interpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invariant generation and bounded model checking. A number of recent papers studies interpolation in various theories and also extraction of smaller interpolants from proofs. In particular, there are several algorithms for extracting of interpolants from so-called local proofs. The main contribution of this paper is a technique of minimising interpolants based on transformations of what we call the "grey area" of local proofs. Another contribution is a technique of transforming, under certain common conditions, arbitrary proofs into local ones. Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear integer arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants. <s> BIB004 </s> A Survey of Satisfiability Modulo Theory <s> Craig Interpolation <s> Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formulae. In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Contrary to existing approaches, this scheme neither limits the inferences done by the SMT solver, nor does it transform the proof tree before extracting interpolants. Our scheme works for the combination of uninterpreted functions and linear arithmetic but is extendable to other theories. The scheme is implemented in the interpolating SMT solver SMTInterpol. <s> BIB005 </s> A Survey of Satisfiability Modulo Theory <s> Craig Interpolation <s> We describe a compositional approach to Craig interpolation based on the heuristic that simpler proofs of special cases are more likely to generalize. The method produces simple interpolants because it is able to summarize a large set of cases using one relatively simple fact. In particular, we present a method for finding such simple facts in the theory of linear rational arithmetic. This makes it possible to use interpolation to discover inductive invariants for numerical programs that are challenging for existing techniques. We show that in some cases, the compositional approach can also be more efficient than traditional lazy SMT as a decision procedure. <s> BIB006 </s> A Survey of Satisfiability Modulo Theory <s> Craig Interpolation <s> Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model checking, CEGAR, SMT, etc., in which the hardest part is how to synthesize interpolants. Various work for discovering interpolants for propositional logic, quantifier-free fragments of first-order theories and their combinations have been proposed. However, little work focuses on discovering polynomial interpolants in the literature. In this paper, we provide an approach for constructing non-linear interpolants based on semidefinite programming, and show how to apply such results to the verification of programs by examples. <s> BIB007 </s> A Survey of Satisfiability Modulo Theory <s> Craig Interpolation <s> Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer "simple" refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process. <s> BIB008
The following conjunction is satisfiable if and only if it is possible to go from a model x 0 of A to a model x n of B by a sequence of transitions (τ i ) 1≤i≤n : In program analysis, A typically expresses a precondition, ¬B a postcondition, x i the variables of the program after i instruction steps, and τ i the semantics of the i-th instruction in a sequence, and the formula is unsatisfiable if and only if B is always true after executing that sequence of instruction starting from A. A hand proof of unsatisfiability would often consist in exhibiting predicates I 1 ( x 1 ), . . . , I n−1 ( x n−1 ), such that, posing I 0 = A and I n = B, for all 0 ≤ i < n, along with proofs of these local inductiveness implications. A SMT-solver, in contrast, produces a monolithic proof of unsatisfiability of (23): it mixes variables from different x i , that is, in program analysis, from different times of the execution of the program. It is however possible to obtain instead a sequence I i satisfying (24) by post-processing that proof  BIB005 BIB001 . In any theory admitting quantifier elimination, such a sequence must exist: defines the strongest sequence of valid interpolants; the weakest is: The strongest sequence corresponds to computing exactly the sequence of sets of states reachable by τ 1 , then τ 2 • τ 1 etc. from A. Binary interpolation consists in: given A and B, produce I such that in which case, if the theory admits quantifier elimination, ∃ x 0 A( x 0 , x 1 ) and ∀ x 2 B( x 1 , x 2 ) are respectively the strongest and weakest interpolant, and any One of the main uses of Craig interpolation in program analysis is to synthesize inductive invariants, for instance by counterexample-guided abstraction refinement in predicate abstraction (CEGAR) BIB002 or property-guided reachability (PDR). Interpolants obtained by quantifier elimination are too specific (overfitting): for instance, strongest interpolants exactly fit the set of states reachable in 1, 2, . . . steps. It has been argued that interpolants likely to be useful as inductive invariants should be "simple" -short formula, with few "magical constants". A variety of approaches have been proposed for getting such interpolants BIB006 BIB003 BIB008 or to simplify existing interpolants BIB004 . Example 9. Consider the interpolation problem A ⇒ I, I ⇒ ¬B (Fig. 1) : SMTInterpol 14 and MathSAT 15 produce I △ = x ≤ 1 ∨ y ≤ 1. This is due to the way these tools produce interpolants from DPLL(T) proofs of unsatisfiability. On this example, a DPLL(T) solver will essentially analyze both branches of A 1 ∨A 2 . The first branch yields A 1 ⇒ ¬B. Finding I 1 such that A 1 ⇒ I 1 and I 1 ⇒ ¬B amounts to finding a separating hyperplane between these two convex polyhedra; I 1 △ = x ≤ 1 works. Similarly, I 2 such that A 1 ⇒ I 2 and I 2 ⇒ ¬B can be I 2 △ = y ≤. I 1 ∨ I 2 is then produced as interpolant. Yet, a search for a single separating hyperplane may produce x + 2y ≤ 9, or x + y ≤ 5. The second hyperplane may seem preferable according to a criterion limiting the magnitude of integer constants. It is easy to see that if one can find interpolants for arbitrary conjunctions A, B such that A ⇒ ¬B, one can find them between arbitrary quantifier-free formulas, by putting them into DNF. Because such a procedure would be needlessly costly due to disjunctive normal forms, the usual approach is to post-process a DPLL(T) proof that A( x, y)∧B( y, z) is unsatisfiable  BIB005 . First, interpolants are derived for all theory lemmas: each lemma expresses that a conjunction of atoms from the original formula is unsatisfiable, these atoms can thus be divided into a conjunction α of atoms from A and a conjunction β of atoms from B, and an interpolant I is derived for α ⇒ ¬β. Then, these interpolants are combined following the resolution proof of the solver. This is how the interpolants from Ex. 9 were produced by the solvers. The problem is therefore: given A( x, y) ∧ B( y, z) unsatisfiable, where A and B are conjunctions, how do we find I( y) such that A ⇒ I and I ⇒ ¬B? If the theory is linear rational arithmetic, this amounts to finding a separating hyperplane between the polyhedra A and B. Let us note Each a ′ i (resp. b i is infinitesimal; all other numbers are assumed to be real. y ≥ (x R , x ǫ ) with x ǫ > 0 and y ∈ R expresses that y > x R . Since A∧B is unsatisfiable, by Farkas' lemma, there exists an unsatisfiability witness (λ i ), (µ j ), such that Such coefficients can in fact be read off the simplex tableau from the most common way of implementing a DPLL(T) solver for linear real arithmetic, as described in Sec. 2.3. Then the following is a valid interpolant (recall that the right-hand side can contain infinitesimals, leading to >): For polynomial arithmetic, one approach replaces nonnegative reals by sumsof-squares of polynomials, and Farkas' lemma by Positivstellensatz BIB007 . Another difficulty is posed for certain theories, for which the solving process involves generating lemmas introducing atoms not present in the original. Consider the approaches for linear integer arithmetic described in Section 2.4: except for branch-and-bound, all can generate new constraints involving any of the unknowns, without respecting the original partition of variables. This poses a problem for interpolation: if interpolating for A(x, y) ∧ B(y, z) over linear real arithmetic, we can rely on all atomic propositions being linear inequalities either over x, y or y, z, but here, we have new atomic propositions that can involve both x, z. Special theory-dependent methods are needed to get rid of these new propositions when processing the DPLL(T) proof into an interpolant  BIB005 .