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
. 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
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.