Interpolants in Nonlinear Theories Over the Reals
 6 Citations
 1.2k Downloads
Abstract
We develop algorithms for computing Craig interpolants for firstorder formulas over real numbers with a wide range of nonlinear functions, including transcendental functions and differential equations. We transform proof traces from \(\delta \)complete decision procedures into interpolants that consist of Boolean combinations of linear constraints. The algorithms are guaranteed to find the interpolants between two formulas A and B whenever \(A \wedge B\) is not \(\delta \)satisfiable. At the same time, by exploiting \(\delta \)perturbations one can parameterize the algorithm to find interpolants with different positions between A and B. We show applications of the methods in control and robotic design, and hybrid system verification.
Keywords
Decision Procedure Nonlinear Theory Interval Arithmetic Execution Trace Proof Tree1 Introduction
Verification problems of complex embedded software can be reduced to solving logic formulas that contain continuous, typically nonlinear, real functions. The framework of \(\delta \)decision procedures [19, 21] establishes that, under reasonable relaxations, nonlinear SMT formulas over the reals are in principle as solvable as SAT problems. Indeed, using solvers for nonlinear theories as the algorithmic engines, straightforward bounded model checking has already shown promise on nonlinear hybrid systems [9, 28]. Naturally, for enhancing performance, more advanced reasoning techniques need to be introduced, extending SMT towards general quantifier elimination. However, it is wellknown that quantifier elimination is not feasible for nonlinear theories over the reals. The complexity of quantifier elimination for real arithmetic (i.e., polynomials only) has a doubleexponential lower bound, which is too high for most applications; when transcendental functions are further involved, the problem becomes highly undecidable.
Craig interpolation provides a weak form of quantifier elimination. Given two formulas A and B, such that \(A~{\wedge }~B\) is unsatisfiable, an interpolant I is a formula satisfying: (1) \(A~{\Rightarrow }~I\), (2) \(B~{\wedge }~I~{\Rightarrow }~{\bot }\), and (3) I contains only variables common to A and B. It has found many applications in verifications: as an heuristic to compute inductive invariant [30, 33, 35], for predicate discovery in abstraction refinement loops [32], inter procedural analysis [2, 3], shape analysis [1], faultlocalisation [10, 17, 39], and so on.
In this paper, we present methods for computing Craig interpolants in expressive nonlinear theories over the reals. To do so, we extract interpolants from proofs of unsatisfiability generated by \(\delta \)decision procedures [22] that are based on Interval Constraint Propagation (ICP) [6]. The proposed algorithms are guaranteed to find the interpolants between two formulas A and B, whenever \(A~{\wedge }~B\) is not \(\delta \)satisfiable.
The framework of \(\delta \)decision procedures formulates a relaxed notion of logical decisions, by allowing onesided \(\delta \)bounded errors [18, 19]. Instead of asking whether a formula has a satisfiable assignment or not, we ask if it is “\(\delta \) satisfiable” or “unsatisfiable”. Here, a formula is \(\delta \)satisfiable if it would be satisfiable under some \(\delta \) perturbation on the original formula [18]. On the other hand, when the algorithm determines that the formula is “unsatisfiable”, it is a definite answer and no numerical error can be involved. Indeed, we can extract proofs of unsatisfiability from such answers, even though the search algorithms themselves involve numerical errors [22]. This is accomplished by analyzing the execution trace of the search tree based on the ICP algorithm.

(Prune) Use interval arithmetic to maintain overapproximations of the solution sets, so that one can “prune” out the part of the state space that does not contain solutions.

(Branch) When the pruning operation does not make progress, one performs a depthfirst search by “branching” on variables and restart pruning operations on a subset of the domain.
When a formula is unsatisfiable, the execution trace of the algorithm generates a (potentially large) proof tree that divides the space into small hypercubes and associating a constraint to each hypercube [22]. The interpolation algorithm can essentially traverse this proof tree to construct the interpolant. To each leaf in the proof, we associate \(\top \) or \(\bot \) depending on the source of the contradiction. The inner nodes of the proof tree correspond to case splits and are handled in a manner reminiscent of Pudlák’s algorithm [37]. Common variables are kept as branching points and A,B local variables are eliminated. A simple example of the method is as follows:
Example 1
Let \(A: y~{\ge }~x{^2}\) and \(B: y~{\le }~\cos (x) + 0.8\) be two constraints over the domain \(x~{\in }~[1,1]\), \(y{\in }[1,1]\). A \(\delta \)decision procedure uses A and B to contract the domains of x and y by removing the parts that be shown empty using interval arithmetic. Figure 1 shows a sequence of contraction proving the unsatisfiability of the formula. As the contraction occurs, we color the region of the space by the color of the opposite formula. When the interval constraint propagation has finished, the initial domain is associated to either A or B. The interpolant I is composed of the parts corresponding to A. We will compute that I is \(y~{\ge }~0~{\wedge }~(0.26~{\le }~y~{\vee }~(y~{\le }~0.26~{\wedge }~0.51~{\le }~x~{\le }~0.51))\).
We have implemented the algorithms in the SMT solver dReal [20]. We show examples of applications from various domains such as control and robotic design, and hybrid system verification.
Related Work. Our algorithm is very similar to the algorithm for propositional interpolation studied by Pudlák [37]. Craig interpolation for real or integer arithmetic has focused on the linear fragment with LA(\(\mathbb {R}\)) [31, 38] and LA(\(\mathbb {Z}\)) [8, 24]. Dai et al. [15] present a method to generate interpolants for polynomial formula. Their method use semidefinite programming to search for a polynomial interpolant and it is complete under the Archimedean condition. In fact, the Archimedean condition imposes similar restrictions as \(\delta \)decidability, e.g., the variables over bounded domains and limited support for strict inequalities. Our method is more general in that it handles nonlinear fragments over \(\mathbb {R}\) that include transcendental functions and solution functions of ordinary differention equations. Existing tools to compute interpolation such as MathSat5 [12], Princess [8], SmtInterpol [11], and Z3 [34] focus on linear arithmetic. We are the first to provide interpolation in nonlinear theories.
Outline. In Sect. 2, we review notions related to interpolation, nonlinear arithmetic over the Reals and \(\delta \)decision procedures. In Sect. 3, we introduce our interpolation algorithm. In Sect. 4, we present and evaluate our implementation. We conclude and sketch future research direction in Sect. 5.
2 Preliminaries

\(A~{\Rightarrow }~I\);

\(B~{\wedge }~I~{\Rightarrow }~{\bot }\);

\(fv(I)~{\subseteq }~fv(A)~{\cap }~fv(B)\) where \(fv(\cdot )\) returns the free variables in a formula.
Intuitively, I provides an overapproximation of A that is still precise enough to exhibit its conflict with B. In particular, I involves only variables (geometrically, dimensions) that are shared by A and B.
Notation 1
We use the metalevel symbol \(\Rightarrow \) as a shorthand for logical implications in texts. In the proof rules that we will introduce shortly, \(\vdash \) is used as the formal symbol with the standard interpretation as logical derivations.
\(\delta \) Complete Decision Procedures. We consider firstorder formulas interpreted over the real numbers. Our special focus is formulas that can contain arbitrary nonlinear functions that are Type 2 computable [7, 40]. Intuitively, Type 2 computability corresponds to numerical computability. For our purpose, it is enough to note that this set of functions consist of all common elementary functions, as well as solutions of Lipschitzcontinuous ordinary differential equations.
Proofs from Constraint Propagation. A detailed description of proof extraction from \(\delta \)decision procedure is available in [22]. Here, we use a simplified version.Intuitively, the proof of unsatisfiability recursively divides the solution space to small pieces, until it can prove (mostly using interval arithmetic) that every small piece of the domain contains no solution of the original system. Note that in such a proof, the difference between pruning and branching operations become blurred for the following reason.
Pruning operations show that one part of the domain can be discarded because no solution can exist there. Branching operations split the domain along one variable, and generates two subproblems. From a proof perspective, the difference between the two kinds of operations is simply whether the emptiness in one part of domain follows from a simple properties of the functions (theory lemma), or requires further derivations. Indeed, as is shown in [22], the simple proof system in Fig. 2 is enough for establishing all theorems that can be obtained by \(\delta \)decision procedures. The rules can be explained as follows.

The Split rules divides the solution space into two disjoint subspaces.

The theory lemmas (ThLem) are the leaves of the proof. They are used when the solver managed to prove the absence of solution in a given subspace.

The Weakening rule extracts those conjunct out of the main formula.
3 Interpolants in Nonlinear Theories
3.1 Core Algorithms
Our method for constructing disjunctive linear interpolants takes two inputs: a proof tree and a labeling function. The labeling function maps formula and variables to either a, b, or ab. For each proof rule introduced in Fig. 2, we associate some partial interpolants, written in square bracket on the right of the conclusion of the rule. Figure 4 shows these modified versions of the rules.

At the leaf level (rule ThLemI), the tile is in I if c is not part of A, i.e., the contradiction originates from B. If c is in both A and B then it can be considered as either part of A or B. Both cases lead to a correct interpolant.

The WeakeningI rule does not influence the interpolant, it is only required to pick c from \(A~{\wedge }~B\).

The SplitI is the most interesting rule. Splitting the domain essentially defines the bounds of the subsequent domains. Let x be the variable whose domain is split at value p and \(I{_1}\), \(I{_2}\) be the two interpolants for the case when \(x < p\) and \(x~{\ge }~p\). If x occurs in A but not B, then x cannot occur in I. Since x is in A then we know that A implies \(x < p~{\Rightarrow }~I{_1}\) and \(x~{\ge }~p~{\Rightarrow }~I{_2}\). Eliminating x gives \(I = I{_1}~{\vee }~I{_2}\). A similar reasoning applies when x occurs in B but not A and gives \(I = I{_1}~{\wedge }~I{_2}\). When x occurs in both A and B then x is kept in I and acts as a selector for the values of x smaller than p \(I{_1}\) is selected, otherwise \(I{_2}\) applies.
The correctness of our method is shown by the following theorem:
Theorem 1
The rules SplitI, ThLemI, WeakeningI generate a Craig interpolant I from the proof of unsatisfiability of A and B.
Proof
We prove correctness of the rules by induction. To express the inductive invariant, we split the domain \(\varvec{D}\) into the domains \(\varvec{D}_A\) and \(\varvec{D}_B\) which contains only the intervals of the variables occurring in A, B respectively.
At any given point in the proof, the partial interpolant I is an interpolant for the formula A over \(\varvec{D}_A\) and B over \(\varvec{D}_B\). At the root of the proof tree we get an interpolant for the whole domain \(\varvec{D} = \varvec{D}_A~{\wedge }~\varvec{D}_B\).
At the leaves of the proof, or the ThLemI rule, one of the constraints has no solution over the domain. Let’s assume that this constraint comes from A. Then the partial interpolant I is \({\bot }\). We have that \(A~{\wedge }~\varvec{D}_A~{\Rightarrow }~I\) by the semantics of the ThLem rule (\({\bot }{\Rightarrow }{\bot }\)). Trivially, \(B~{\wedge }~\varvec{D}_B~{\wedge }~I~{\Rightarrow }~{\bot }\) and \(fv(I) =~{\emptyset }~{\subseteq }~fv(A)~{\cap }~fv(B)\). When the contradiction comes from B, a similar reasoning applies with \(I={\top }\).
The WeakeningI only serves to select the constraint which causes the contradiction and does not change the invariant.
The SplitI rule is the most complex case. We have to consider whether the variable x which is split come from A, B, or is shared. For instance, if \(x~{\in }~fv(A)\) then the induction step has \(\varvec{D}_{A1} = \varvec{D}_A~{\wedge }~x < p\) and \(\varvec{D}_{A2} = \varvec{D}_A~{\wedge }~x~{\ge }~p\) and \(\varvec{D}_B\) is unchanged. If \(x~{\in }~fv(B)\) then \(\varvec{D}_B\) is affected and \(\varvec{D}_A\) is unchanged. If x is shared then both \(\varvec{D}_A\) and \(\varvec{D}_B\) are affected.
\(\square \)
Example 2
If we look at proof for the example in Fig. 1, we get the proof annotated with the partial interpolants shown in Fig. 5. The final interpolants \(I{_5}\) is \(0{\le }y~{\wedge }~(0.26{\le }y~{\vee }~(y{\le }0.26~{\wedge }~0.51~{\le }~x~{\le }~0.51))\).
Boolean Structure. The method we presented explain how to compute an interpolant for the conjunctive fragment of quantifierfree nonlinear theories over the reals. However, in many cases formula also contains disjunctions. To handle disjunctions, our method can be combined with the method presented by Yorsh and Musuvathi [41] for building an interpolant from a resolution proof where some of the proof’s leaves carry theory interpolants.
Handling ODE Constraints. A special focus of \(\delta \)complete decision procedures is on constraints that are defined by ordinary differential equations, which is important for hybrid system verification. In the logic formulas, the ODEs are treated simple as a class of constraints, over variables that represent both state space and time. Here we elaborate on the proofs and interpolants for the ODE constraints.
3.2 Extensions
For any two formulas A,B which conjunction is unsatisfiable, the interpolant I is not unique. In practice, it is difficult to know a priori what is a good interpolant. Therefore, it is desirable to have the possibility of generating and testing multiple interpolants. We now explain how to get interpolants of different logical strength. An interpolant \(I{_1}\) is stronger than an interpolant \(I{_2}\) iff \(I{_1}~{\Rightarrow }~I{_2}\). Intuitively, a stronger interpolant is closer to A and a weaker interpolant closer to B.
Parameterizing Interpolation Strength. The interpolation method that we propose uses a \(\delta \)decision procedure to build a Craig interpolant. I being an interpolant means that \(A~{\wedge }~{\lnot }I\) and \(B~{\wedge }~I\) are both unsatisfiable. However, these formulas might still be \(\delta \)satisfiable.
In the labelled interpolation system, it is possible to modify the a,b,ab labelling as long as it preserves locality, see [16] for the details. An additional restriction in our case is that we cannot use a projection of constraints at the proof’s leaves. The projection is not computable in nonlinear theories. Therefore, the labelling must enforce that the leaves maps to the interpolants \(\top \) or \(\bot \).
4 Applications and Evaluation
We have implemented the interpolation algorithm in a modified version of the dReal SMT solver.^{1} The proofs produced by dReal can be very large, i.e., gigabytes. Therefore, the interpolants are built and simplified onthefly. The full proof is not kept in memory. We modified the ICP loop and the contractors which are responsible for the pruning steps. The overhead induced by the interpolant generation over the solving time is smaller than 10 %.
Interpolant Sizes. The ICP algorithm implemented in dReal eagerly prunes the domain by applying repeatedly all the constraints. Therefore, it usually generates large proofs often involving all the constraints and all the variables. Interpolation can extract more precise information from the proof. Intuitively, an interpolant which is much smaller than the proof are more likely to be useful in practice. In this test, we try to compare the size of the proof against the size of the interpolants using benchmark from the Flyspeck project [25], certificates for Lyapunov functions in powertrain control systems [27] and the other examples presented in the rest of this section.
We run dReal with a 20 min timeout and generate 1063 interpolants. Out of these, 501 are nontrivial. In Fig. 6 we plot the number of inequalities in the nontrivial interpolants against the size of the proof without the Weakening steps. For similar proofs, we see that the interpolants can be order of magnitude simpler than the proofs and other interpolants obtained by different partitions of the formula. The trivial interpolants still bring information as they mean that the only one side is part of the unsatisfiable core.
Results for the interpolation of ODEs. The [_,_] notation stands for intervals that cover the values for the whole families of examples. The first column indicates the family. The next three columns contains the number of tests in the family, the number of flows and variables in the tests. The last three columns shows the size of the proofs, interpolants, and the solving time.
Family  #tests  #flow  #var  Proof size  Interpolant size  Time 

Airplane control  53  [1,4]  [56,61]  [4213,24249]  [70,10260]  [57 s,178 s] 
Apex  17  1  44  23  [0,22]  [5 s,9 s] 
Bouncing ball  165  2  128  857  [0,28]  [1.6 s,5.5 s] 
Cardiac cells  37  4  71  15  [0,1]  [15 m,20 m] 
Water tanks  68  [4,8]  [18,30]  [6530,225099]  [331,92594]  [7 s,12 m] 
Lane change  15  1  44  24  [0,23]  [19 s,20 s] 
Other tests  142  1  5  2  [0,1]  [0.1 s,1 s] 
Robotic Design. Often, hybrid system verification is used in modelbased design. An expert produces a model of the system which is then analysed. However, it is also possible to extract models directly from the manufacturing designs. As part of an ongoing project about codesign of both the software and hardware component of robots [42], we extract equations from robotic designs. In the extracted models, each structural element is represented by a 3D vector for its position and a unit quaternion for the orientation. The dimension of the elements and the joints connecting them corresponds to equations that relate the position and orientation variables. Active elements, such as motors, also have specific equations associated to them.
This approach provides models faithful to the actual robots, but it has the downside of producing large systems of equations. To verify such systems, we need to simplify them. Due to the presence of trigonometric functions we cannot use quantifier elimination for polynomial systems of equations [13]. However, we use interpolation as an approximation of quantifier elimination.
Let us consider a kinematic model, \({\mathcal {K}}(\varvec{x},\varvec{y},\varvec{z})\) where \(\varvec{x}\) is a set of design and input parameters, \(\varvec{y}\) is the variables that represent the state of each component of the robot, and \(\varvec{z}\) is the variables that represent the parts of the state needed to prove the property of interest. For instance, in the case of a robotic manipulator, \(\varvec{x}\) contain the sizes of each element and the angles of the servo motors and \(\varvec{z}\) is the position of the effector. \(\varvec{y}\) is determined by the designed of the manipulator.
Comparison of the original model of a 1 and 2 degrees of freedom manipulator against approximations obtained using interpolation. For the size of the formulas we report the number of theory atoms in the formula. The last column shows the time dReal takes to compute the interpolants.
Example 3
Consider the simple robotic manipulator show in Fig. 7b. The manipulator has one degree of freedom. It is composed of two beams connected by a revolute joint controlled by a servo motor. The first beam is fixed.
The original system of equations describing this system has 22 variables: 7 for each beam, 7 for the effector, and 1 for the revolute joint. Using the interpolation we obtain a simpler formula with only 4 variables: 3 for the effector’s position and 1 for the joint. Table 2 shows some statistics about the interpolants we obtained using different \(\epsilon \) for a one and a two degrees of freedom manipulators.
5 Conclusion and Future Work
We present an method for computing Craig interpolants for firstorder formulas over real numbers with a wide range of nonlinear functions. Our method transform proof traces from \(\delta \) decision procedures into interpolants consisting of disjunctive linear constraints. The algorithms are guaranteed to find the interpolants between two formulas A and B whenever \(A~{\wedge }~B\) is not \(\delta \)satisfiable. Furthermore, we show how the framework apply to systems of ordinary differential equations. We implemented our interpolation algorithm in the dReal SMTsolver and apply the method to domains such robotic design, and hybrid system verification.
In the future, we plan to expand our work to richer proof systems. The ICP loop produces proof based on interval pruning which results in large, “squarish” interpolants. Using more general proof systems, e.g. cutting planes and semidefinite programming [15], we will be able to get smaller, smoother interpolants. CDCLstyle reasoning for richer theories, e.g., LA(\(\mathbb {R}\)) [36] and polynomial [26], is a likely basis for such extensions. Furthermore, we are interested in investigating the link between classical interpolation and Craig interpolation over the reals. Using methods like spline interpolation and radial basis functions, it maybe possible to build smoother interpolants. We also to extend the our rules to compute interpolants mixed proofs with both integer and real variables.
Footnotes
 1.
Currently available in the branch https://github.com/dzufferey/dreal3/.
References
 1.Albargouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 634–660. Springer, Heidelberg (2015)CrossRefGoogle Scholar
 2.Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: an interpolationbased algorithm for interprocedural verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 39–55. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 3.Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction and interpolationbased software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672–678. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 4.Althoff, M., Dolan, J.M.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Robot. 30(4), 903–918 (2014)CrossRefGoogle Scholar
 5.Bae, K., Krisiloff, J., Meseguer, J., Ölveczky, P.C.: Designing and verifying distributed cyberphysical systems usingmultirate pals: an airplane turning control system case study. sci. comput. program. 103, 13–50 (2015). Selected papers from the First International Workshop on FormalTechniques for SafetyCritical Systems (FTSCS 2012)CrossRefGoogle Scholar
 6.Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming. Elsevier, Amsterdam (2006). chapter 16Google Scholar
 7.Brattka, V., Hertling, P., Weihrauch, K.: A tutorial on computable analysis. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds.) New Computational Paradigms, pp. 425–491. Springer, New York (2008)Google Scholar
 8.Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An interpolating sequent calculus for quantifierfree presburger arithmetic. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 384–399. Springer, Heidelberg (2010)CrossRefGoogle Scholar
 9.Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: An analyzer for nonlinear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 10.Christ, J., Ermis, E., Schäf, M., Wies, T.: Flowsensitive fault localization. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 189–208. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 11.Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 12.Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 13.Collins, G., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation, pp. 174–200. Springer Vienna (1998)Google Scholar
 14.Craig, W.: Linear reasoning. A new form of the herbrandgentzen theorem. J. Symb. Logic 22, 250–268 (1957)MathSciNetCrossRefzbMATHGoogle Scholar
 15.Dai, L., Xia, B., Zhan, N.: Generating nonlinear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 364–380. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 16.D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129–145. Springer, Heidelberg (2010)CrossRefGoogle Scholar
 17.Ermis, E., Schäf, M., Wies, T.: Error invariants. In: Méry, D., Giannakopoulou, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 187–201. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 18.Gao, S., Avigad, J., Clarke, E.M.: Deltacomplete decision procedures for satisfiability over the reals. In: Gramlich et al. [23], pp. 286–300Google Scholar
 19.Gao, S., Avigad, J., Clarke, E.M.: Deltadecidability over the reals. IEEE Computer Society, In: LICS (2012)Google Scholar
 20.Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208–214. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 21.Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo odes. In: FMCAD, IEEE (2013)Google Scholar
 22.Gao, S., Kong, S., Clarke, E.M.: Proof generation from deltadecisions. In: Winkler, F., Negru, V., Ida, T., Jebelean, T., Petcu, D., Watt, S.M., Zaharie, D. (eds.) SYNASC. IEEE (2014)Google Scholar
 23.de Boer, F., Bonsangue, M., Rot, J.: Automated verification of recursive programs with pointers. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 149–163. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 24.Griggio, A., Le, T.T.H., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo linear integer arithmetic. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 143–157. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 25.Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. ArXiv eprints, January 2015Google Scholar
 26.Jovanović, D., de Moura, L.: Solving nonlinear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 27.Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Arechiga, N.: Simulationguided lyapunov analysis for hybrid dynamical systems. In: Fränzle, M., Lygeros, J. (eds.) HSCC. ACM (2014)Google Scholar
 28.Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015)Google Scholar
 29.Liu, B., Kong, S., Gao, S., Zuliani, P., Clarke, E.M.: Parameter synthesis for cardiac cell hybrid models using \(\delta \)decisions. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 99–113. Springer, Heidelberg (2014)Google Scholar
 30.McMillan, K.L.: Interpolation and SATbased model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
 31.McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 32.McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)CrossRefGoogle Scholar
 33.McMillan, K.L.: Interpolants and symbolic model checking. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 89–90. Springer, Heidelberg (2007)CrossRefGoogle Scholar
 34.McMillan, K.L.: Interpolants from Z3 proofs. In: Bjesse, P., Slobodová, A. (eds.) FMCAD. FMCAD Inc. (2011)Google Scholar
 35.McMillan, K.L.: Widening and interpolation. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, p. 1. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 36.McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462–476. Springer, Heidelberg (2009)CrossRefGoogle Scholar
 37.Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic 62(3), 981–998 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
 38.Rybalchenko, A., SofronieStokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007)CrossRefGoogle Scholar
 39.Schäf, M., SchwartzNarbonne, D., Wies, T.: Explaining inconsistent code. In: Meyer, B., Baresi, L., Mezini, M. (eds.) ACM SIGSOFT. ACM (2013)Google Scholar
 40.Weihrauch, K., Analysis, C.: An Introduction (2000)Google Scholar
 41.Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 42.Zufferey, D., Mehta, A., DelPreto, J., SidiroglouDouskos, S., Rinard, M., Rus, D.: Talos: Full stack robot compilation, simulation, and synthesis.Submitted to ICRA 2016 (2016)Google Scholar