A Combination Method for Generating Interpolants

Greta Yorsh and Madan Musuvathi

To appear in Proc. Conf. on Automated Deduction, 2005 (CADE-20, 2005)

Microsoft Research Technical Report, MSR-TR-2004-108, October 2004

We present a combination method for generating interpolants for a class of first-order theories. Using interpolant-generation procedures for individual theories as black-boxes, our method generates interpolants for the combined theory. Our method extends that of McMillan to a class of first-order theories, which we characterize as equality-interpolating Nelson-Oppen theories. We show that this class includes many useful theories such as the quantifier-free theories of uninterpreted functions, linear inequalities over reals, and Lisp structures. Our method provides a way to integrate interpolant generation within existing Nelson-Oppen-style decision procedures (such as Simplify, Verifun, ICS, and CVC-Lite).

We have implemented this method in Zap, a symbolic reasoning engine in development at Microsoft Research.

Click here to access the short version of the paper (CADE-20, 2005):
[PS; PDF]
Click here to access the technical report with proofs (October 2004):
[TR-PDF]
Unfortunately, the technical report published by MSR is no longer available.
The proofs (dated October 2004) can be found in the appendix of this document
[TR-PDF]