Academic
Publications
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic,10.1007/978-3-642-14203-1_33,Angelo Brillout,Daniel Kroening,Philipp Rümme

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic   (Citations: 6)
BibTex | RIS | RefWorks Download
Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis of programs. Interpolants are typically determined by annotating the steps of an unsatisfiability proof with partial interpolants. In this paper, we consider Craig interpolation for full quantifier-free Presburger arithmetic (QFPA), for which currently no efficient interpolation procedures are known. Closing this gap, we introduce an interpolating sequent calculus for QFPA and prove it to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available linear integer arithmetic benchmarks. The results indicate the robustness and efficiency of our proof-based interpolation procedure.
Conference: Conference on Automated Deduction - CADE , pp. 384-399, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...In earlier work, we presented a similar procedure for quantifier-free Presburger arithmetic [2]...
    • ...Interpolating sequents. To extract interpolants from unsatisfiability proofs of A ∧ B, formulae are labelled either with the letter L (“left”) to indicate that they are derived from A or with R (“right”) for formulae derived from B (as in [2])...
    • ...An exhaustive list of rules is given in [2]...
    • ...Correctness. The calculus consisting of the rules in Fig. 1, the arithmetic rules of [2], and axiom (1) generates correct interpolants...
    • ...In particular, the sequent ΓL ,Γ R � ΔL ,Δ R is valid in this case. As shown in [2], Lem...
    • ...With the help of results in [5,2], it is easy to see that our calculus is sound and complete for PA+UP, and can in fact be turned into a decision procedure...
    • ...The proof can then be closed using propositional rules, complementary literals, and arithmetic reasoning [2]...
    • ...where (i) D, E ∈{ L, R} and F ∈{ D, E} are arbitrary labels, (ii) the proof Q only uses the rules red-right, mul-right, ipi-right, and-right-l ,a nd close-eq-right applied to an equality derived from ¯ s − ¯ . =0 (see [2] for definitions of the rules), and (iii) all-left and ex-right are not applied in any other places in P .T henI is a PAID+UP formula up to normalisation of guards...
    • ...where (i) D, E ∈{ L, R} and F ∈{ D, E} are arbitrary labels, (ii) R ∈{ D, E} implies F = R, (iii) the proof Q only uses the rules red-right, mul-right, ipiright, and-right-l ,a ndclose-eq-right applied to an equality derived from ¯ s1 . =¯ s2 (see [2]), (iv) all-left and ex-right are not applied in any other places in P .T henI is a PAID+UFp formula up to normalisation of guards...
    • ...Related work. For work on interpolation in pure quantifier-free Presburger arithmetic, see [2]...

    Angelo Brilloutet al. Beyond Quantifier-Free Interpolation in Extensions of Presburger Arith...

    • ...Consequently, the problem of computing interpolants in SMT has received a lot of interest in the last years (e.g., [14,17,19,11,4,10,13,7,8,3,12])...
    • ...The work in [3] was the first to present an interpolation algorithm for the full LA(Z) (augmented with divisibility predicates) which was not based on quantifier elimination...
    • ...In particular, some of the interpolation rules of [3] might result in an exponential blow-up in the size of the interpolants wrt...
    • ...interpolation procedure, and allows for producing interpolants which are much more compact than those generated by the algorithm of [3]...
    • ...Similarly to previous work on LA(Q) and LA(Z) [14,3], we produce interpolants by annotating each step of the proof of unsatisfiability of A ∧ B, such that the annotation for the root of the proof (deriving an inconsistent inequality (c ≤ 0) with c ∈ Z >0 ) is an interpolant for (A, B). 148 A. Griggio, T.T.H...
    • ...Notice that the first three rules correspond to the rules for LA(Q) given in [14], whereas Strengthen is a reformulation of the k-Strengthen rule given in [3]...
    • ...Such restriction has been put only for simplifying the proofs of correctness, and it is not present in the original k-Strengthen of [3]...
    • ...We compare MATHSAT with all the other interpolant generators for LA(Z) which are available (to the best of our knowledge): IPRINCESS [3], 8 INTERPOLATINGOPENSMT...

    Alberto Griggioet al. Efficient Interpolant Generation in Satisfiability Modulo Linear Integ...

    • ...Brillout et al. [2] define a complete interpolating sequent calculus for QFPA...
    • ...‐ the theorem prover iPrincess [2], which implements an interpolating decision procedure for QFPA based on a sequent calculus, ‐ the SMT-solver SmtInterpol, 1 a recently released interpolating decision procedure for linear integer arithmetic that uses an architecture similar to the one in Foci [11], ‐ quantifier elimination (QE) procedures, which can be used to generate interpolants as illustrated in Sect...
    • ...On such interpolation problems, QE naturally performs very well; with an increasing number of local symbols, the performance of QE quickly degrades (also see [2] for a discussion of this phenomenon)...

    Daniel Kroeninget al. Interpolating Quantifier-Free Presburger Arithmetic

    • ...Following the subtyping rules of the LSP [14], the new state is described by Equation 2, wherePostmi is the postcondition ofmi andv 0 is a valuation for all variables in state s1. Checking and simplifying these equations can be done by employing recent SMT solvers such as [6, 18]...

    Mihai Balint. Automatic inference of abstract type behavior

    • ...Interpolation was proposed for abstraction refinement in software model checking, first for propositional logic and propositional satisfiability [25], and then for quantifier-free fragments of first-order theories, their combinations, and satisfiability modulo theories [18,26,35,21,11,12,17,6,7,9]...
    • ...Considered theories include equality [26,16], linear rational arithmetic [26,21], Presburger or linear integer arithmetic [21,6], or fragments thereof [12], and arrays without extensionality [21,7,8]...
    • ...In these papers the theory reasoning is done either by specialized sequent-style inference systems [18,26,6,7] or by satisfiability procedures, such as congruence closure for equality [16], integrated in a DPLL(T ) framework [35,11,12,17]...
    • ...Since [25], approaches to interpolation work by annotating each clause C in ar efutation ofA and B with auxiliary formulæ, unnamed in [25,26], named C-interpolants in [23], and partial interpolants in [35,15,6]: 4 M.P...

    Maria Paola Bonacinaet al. On Interpolation in Decision Procedures

Sort by: