2008/11/21 by Angelo Brillout, Daniel Kroening, Brillout, Angelo +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Numerical Methods and Algorithms #Polynomial and algebraic computation #Symbolic Computation (cs.SC) #cs.LO #cs.SC
paper · pdf · doi:10.48550/arxiv.0811.3521
15 pages, 1 algorithm, 1 figure
arxiv created 2008/11/21 · openalex publication_date 2008/11/21 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.