Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)
Abstract
Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) extensional arrays (QPA+AR). We prove that none of these combinations can be effectively interpolated without the use of quantifiers, even if the input formulae are quantifier-free. We go on to identify fragments of QPA+UP and QPA+UF with restricted forms of guarded quantification that are closed under interpolation. Formulae in these fragments can easily be mapped to quantifier-free expressions with integer division. For QPA+AR, we formulate a sound interpolation procedure that potentially produces interpolants with unrestricted quantifiers.
Cite
@article{arxiv.1011.1036,
title = {Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)},
author = {Angelo Brillout and Daniel Kroening and Philipp Ruemmer and Thomas Wahl},
journal= {arXiv preprint arXiv:1011.1036},
year = {2015}
}
Comments
extended version (including proofs, complete rules listings, etc) of a VMCAI 2011 proceedings version