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.

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Daniel Kroening, Jérôme Leroux, Philipp Rümmer
• Keywords: Automated Reasoning, Expensive Quantifier Elimination, Interpolation, LPAR 2010, Quantifier Elimination