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
was
shown
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 endeavors 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.