Craig interpolation has become a versatile tool in formal verification,
  used for instance to generate program assertions that serve as candidates
  for loop invariants. In this paper, we consider Craig interpolation for
  quantifier-free Presburger arithmetic (QFPA). Until recently,
  quantifier elimination was the only available interpolation method for
  this theory, which is, however, known to be potentially costly and
  inflexible. We introduce an interpolation approach based on a sequent
  calculus for QFPA that determines interpolants by annotating the steps of
  an unsatisfiability proof with partial interpolants.  We prove our
  calculus 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 Presburger arithmetic benchmarks.
  The results document the robustness and efficiency of our interpolation
  procedure.
  Finally, we compare the procedure against alternative interpolation
  methods, both for QFPA and linear rational arithmetic.

  This paper is an extended version of a publication that appeared at
  IJCAR.