## Presburger Arithmetic Interpolation

*Presburger Arithmetic* (PA) is the first-order theory of linear
operations on integers: it permits addition, constant multiplication, and
comparison for equality and inequality and is, of course, closed under
Boolean operations. The logic naturally allows modeling of transition
relations of many programs manipulating integers. Determining the
reachability of errors up to a certain depth (*Bounded Model
Checking*) then amounts to a PA satisfiability problem. PA is known to
be decidable via quantifier elimination (QE) and integer congruence
reasoning.

Some of the many uses of *interpolation
*include the computation of local program invariants, and the
overapproximation of image computations (to make bounded model checking
complete). It turns out that QE can be used to determine interpolants of
implications in PA, i.e. given A
⇒ B, a
formula I such
that A
⇒ I
and I
⇒ B. In fact one can
determine strongest and weakest interpolants this way. But QE is not only
expensive to perform: useful and compact interpolants often lie in the
"middle" between the strongest and weakest, so we would like to have more
flexibility.

A recent and ongoing project attempts to determine interpolants in a
different way: by extracting them from a proof of A ⇒ B. To
this end, we have
extended Philipp Ruemmer's
sequent calculus for PA to generate interpolants. The idea is to augment
the calculus rules by partial interpolant information that amounts, at the
root of a closed proof, to an actual interpolant. The crux of integer
arithmetic interpolation arises from the fact that systems of equalities
and inequalities are often harder to solve over the integers than over the
rationals or reals, since we do not have division at our disposal. Instead,
we must use rounding
and strengthening of inequalities,
which simulates the integer congruence reasoning used in the original
decidability proof for PA. These operations are summarized in a special
rule, Strengthen, in our
interpolating calculus. We have shown the calculus sound and complete for
interpolation problems for quantifier-free Presburger arithmetic.
Preliminary experimental results demonstrate the robustness of this
interpolation procedure compared to QE-based interpolation (the only extant
alternative method), both in terms of interpolation time and interpolant
size. [BKRW10]

The interpolation engine is being implemented in a tool
called iPrincess,
on top of Philipp Ruemmer's theorem
prover Princess.
The goal is to link it to a model checker such
as Wolverine, in order to
apply the result to verification problems for C programs manipulating
integers. Turns out C programs tend to have arrays! We are thus currently
extending the theory of our calculus by uninterpreted predicates and
functions. They allow us in turn to model arrays using (partially
interpreted) functions select
and store, which simulate array
access operations.

Collaborators: Angelo Brillout, Daniel Kroening, Philipp Ruemmer.