arXiv subjects

Angelo Brillout

Publications and source records attributed to Angelo Brillout.

2 recordsLinked to original sources

arXiv2010

Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)

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.

cs.LO↗

arXiv2008

Craig Interpolation for Quantifier-Free Presburger Arithmetic

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.

cs.LO↗