An interpolating sequent calculus for quantifier-free presburger arithmetic

Abstract

Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis of programs. Interpolants are typically determined by annotating the steps of an unsatisfiability proof with partial interpolants. In this paper, we consider Craig interpolation for full quantifier-free Presburger arithmetic (QFPA), for which currently no efficient interpolation procedures are known. Closing this gap, we introduce an interpolating sequent calculus for QFPA and prove it to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available linear integer arithmetic benchmarks. The results indicate the robustness and efficiency of our proof-based interpolation procedure. © 2010 Springer-Verlag.