Flexible Interpolation with Local Proof Transformations

TitleFlexible Interpolation with Local Proof Transformations
Publication TypeConference Paper
Year of Publication2010
AuthorsBruttomesso, R., Rollini S.F., Sharygina Natasha, and Tsitovich A.
Conference NameInternational Conference of Computer Aided Design (ICCAD)
PublisherIEEE Computer Society
Conference LocationSan Jose, USA

Model checking based on Craig's interpolants ultimately relies on efficient engines, such as SMT-solvers, to log proofs of unsatisfiability and to derive the desired interpolant by means of a set of algorithms known in literature. These algorithms, however, are designed for proofs that do not contain mixed predicates. In this paper we present a technique for transforming the propositional proof produced by an SMT-solver in such a way that mixed predicates are eliminated. We show a number of cases in which mixed predicates arise as a consequence of state-of-the-art solving procedures (e.g. lemma on demand, theory combination, etc.). In such cases our technique can be applied to allow the application of known interpolation algorithms. We demonstrate with a set of experiments that our approach is viable.

Full Text