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 AB, a formula I such that AI and IB. 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 AB. 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.