Craig Interpolation for Quantifier-Free Presburger Arithmetic

Simple item page
dc.creatorBrillout, Angelo
dc.creatorKroening, Daniel
dc.creatorWahl, Thomas
dc.date2008-11-21
dc.date.accessioned2026-07-07T10:20:06Z
dc.date.available2026-07-07T10:20:06Z
dc.descriptionCraig 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.
dc.description15 pages, 1 algorithm, 1 figure
dc.identifierhttps://arxiv.org/abs/0811.3521
dc.identifierhttp://arxiv.org/abs/0811.3521
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/174744
dc.subjectLogic in Computer Science
dc.subjectSymbolic Computation
dc.titleCraig Interpolation for Quantifier-Free Presburger Arithmetic
dc.typetext

Files

Collections

arXiv