Paper Info
Title
Craig interpolation in the presence of non-linear constraints
Abstract
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.
Year
DOI
Venue
2011
10.1007/978-3-642-24310-3_17
FORMATS
Keywords
Field
DocType
linear inequality,verification area,craig interpolants,craig interpolation,existing smt solver,basic solver,non-linear constraint,ci construction,suitable cis,construction rule
Discrete mathematics,Local consistency,Uninterpreted function,Computer science,Propositional calculus,Decidability,Theoretical computer science,Solver,Linear inequality,Satisfiability modulo theories,Craig interpolation
Conference
Volume
ISSN
Citations 
6919
0302-9743
8
PageRank 
References 
Authors
0.48
11
2
Name
Order
Citations
PageRank
Stefan Kupferschmid1727.05
Bernd Becker280.48