Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
A Combination Method for Generating Interpolants

Greta Yorsh and Madanlal Musuvathi

Abstract

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 modularly generates interpolants for the combined theory. Our combination method applies for a broad class of first-order theories, which we characterize as equality-interpolating Nelson-Oppen theories. This class includes many useful theories such as the quantifier-free theories of uninterpreted functions, linear inequalities over reals, and Lisp structures. The combination method can be implemented within existing Nelson-Oppen-style decision procedures (such as Simplify, Verifun, ICS, CVC-Lite, and Zap).

Details

Publication typeInproceedings
Published inin CADE 2005: Twentieth International Conference on Automated Deduction.
URLhttp://www.springer-ny.com/
Pages18
NumberMSR-TR-2004-108
InstitutionMicrosoft Research
PublisherSpringer-Verlag
> Publications > A Combination Method for Generating Interpolants