Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis. Interpolants are typically determined by annotating the stepsof an unsatisfiability proof with partial interpolants. In this paper, we consider Craig interpolation for full quantifier-free Presburger arithmetic (QFPA), for which currently no ecient interpolation procedures are known. Closing this gap, we introduce an interpolating sequent calculus for QFPA and prove it to be sound and complete. We then add uninterpreted predicates to the calculus, thus extending it to important theories such as arrays and uninterpreted functions. We demonstrate the efficiency of our interpolation procedure on a large range of publicly available benchmarks.

%8 16/07/2010