Craig Interpolation in the Presence of Non-linear Constraints

An increasing number of applications in particular in the verification area leverages Craig interpolation. Craig interpolants (CIs) can be computed for many different theories such as: propositional logic, linear inequalities over the reals, and the combination of the preceding theories with uninterpreted function symbols. To the best of our knowledge all previous tools that provide CIs are addressing decidable theories. With this paper we make Craig interpolation available for an in general undecidable theory that contains Boolean combinations of linear and non-linear constraints including transcendental functions like sin(·) and cos(·). Such formulae arise e.g. during the verification of hybrid systems. We show how the construction rules for CIs can be extended to handle non-linear constraints. To do so, an existing SMT solver based on a close integration of SAT and Interval Constraint Propagation is enhanced to construct CIs on the basis of proof trees. We provide first experimental results demonstrating the usefulness of our approach: With the help of Craig interpolation we succeed in proving safety in cases where the basic solver could not provide a complete answer. Furthermore, we point out the (heuristic) decisions we made to obtain suitable CIs and discuss further possibilities to increase the flexibility of the CI construction.