Interpolating Quantifier-Free Presburger Arithmetic

9 years 7 months ago
Interpolating Quantifier-Free Presburger Arithmetic
Craig interpolation has become a key ingredient in many symbolic model checkers, serving as an approximative replacement for expensive quantifier elimination. In this paper, we focus on an interpolating decision procedure for the full quantifier-free fragment of Presburger Arithmetic, i.e., linear arithmetic over the integers, a theory which is a good fit for the analysis of software systems. In contrast to earlier procedures based on quantifier elimination and the Omega test, our approach uses integer linear programming techniques: relaxation of interpolation problems to the rationals, and a complete branch-and-bound rule tailored to efficient interpolation. Equations are handled via a dedicated polynomial-time sub-procedure. We have fully implemented our procedure on top of the SMTsolver OpenSMT and present an extensive experimental evaluation.
Daniel Kroening, Jérôme Leroux, Phili
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where LPAR
Authors Daniel Kroening, Jérôme Leroux, Philipp Rümmer
Comments (0)