Craig Interpolation for Quantifier-Free Presburger Arithmetic

TL;DR

This paper introduces a complete and efficient Craig interpolation method for quantifier-free Presburger arithmetic, enhancing software verification techniques by providing a novel convex variable projection and a polynomial-time derivation process.

Contribution

The paper presents the first complete interpolation procedure for full quantifier-free Presburger arithmetic, combining convex variable projection with equalities, and ensuring low complexity.

Findings

Interpolation derivation has low-degree polynomial complexity.

Method is typically fast in practice.

Enhances verification by accelerating fixpoint computations.

Abstract

Craig interpolation has become a versatile algorithmic tool for improving software verification. Interpolants can, for instance, accelerate the convergence of fixpoint computations for infinite-state systems. They also help improve the refinement of iteratively computed lazy abstractions. Efficient interpolation procedures have been presented only for a few theories. In this paper, we introduce a complete interpolation method for the full range of quantifier-free Presburger arithmetic formulas. We propose a novel convex variable projection for integer inequalities and a technique to combine them with equalities. The derivation of the interpolant has complexity low-degree polynomial in the size of the refutation proof and is typically fast in practice.