Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(5)
Formal Verification
presburger arithmetic
Safety Analysis
Sequent Calculus
Theorem Prover
Subscribe
Academic
Publications
An Interpolating Sequent Calculus for QuantifierFree Presburger Arithmetic
An Interpolating Sequent Calculus for QuantifierFree Presburger Arithmetic,10.1007/9783642142031_33,Angelo Brillout,Daniel Kroening,Philipp Rümme
Edit
An Interpolating Sequent Calculus for QuantifierFree Presburger Arithmetic
(
Citations: 6
)
BibTex

RIS

RefWorks
Download
Angelo Brillout
,
Daniel Kroening
,
Philipp Rümmer
,
Thomas Wahl
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 quantifierfree
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 proofbased interpolation procedure.
Conference:
Conference on Automated Deduction  CADE
, pp. 384399, 2010
DOI:
10.1007/9783642142031_33
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.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
www.informatik.unitrier.de
)
(
dx.doi.org
)
More »
Citation Context
(5)
...In earlier work, we presented a similar procedure for quantifierfree 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 redright, mulright, ipiright, andrightl ,a nd closeeqright applied to an equality derived from ¯ s − ¯ . =0 (see [
2
] for definitions of the rules), and (iii) allleft and exright 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 redright, mulright, ipiright, andrightl ,a ndcloseeqright applied to an equality derived from ¯ s1 . =¯ s2 (see [
2
]), (iv) allleft and exright 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 quantifierfree Presburger arithmetic, see [
2
]...
Angelo Brillout
,
et al.
Beyond QuantifierFree 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 blowup 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 kStrengthen rule given in [
3
]...
...Such restriction has been put only for simplifying the proofs of correctness, and it is not present in the original kStrengthen 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 Griggio
,
et 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 SMTsolver 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 Kroening
,
et al.
Interpolating QuantifierFree 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 quantifierfree fragments of firstorder 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 sequentstyle 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 Cinterpolants in [23], and partial interpolants in [35,15,
6
]: 4 M.P...
Maria Paola Bonacina
,
et al.
On Interpolation in Decision Procedures
References
(17)
CSIsat: Interpolation for LA+EUF
(
Citations: 13
)
Dirk Beyer
,
Damien Zufferey
,
Rupak Majumdar
Published in 2008.
Interpolant Generation for UTVPI
(
Citations: 5
)
Alessandro Cimatti
,
Alberto Griggio
,
Roberto Sebastiani
Conference:
Conference on Automated Deduction  CADE
, pp. 167182, 2009
Linear Reasoning. A New Form of the HerbrandGentzen Theorem
(
Citations: 129
)
William Craig
Journal:
Journal of Symbolic Logic  JSYML
, vol. 22, no. 3, pp. 250268, 1957
Firstorder logic and automated theorem proving
(
Citations: 427
)
Unknown
Published in 1990.
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
(
Citations: 17
)
Himanshu Jain
,
Edmund M. Clarke
,
Orna Grumberg
Conference:
Computer Aided Verification  CAV
, pp. 254267, 2008
Sort by:
Citations
(6)
Beyond QuantifierFree Interpolation in Extensions of Presburger Arithmetic
(
Citations: 3
)
Angelo Brillout
,
Daniel Kroening
,
Philipp Rümmer
,
Thomas Wahl
Conference:
Verification, Model Checking and Abstract Interpretation  VMCAI
, pp. 88102, 2011
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
Alberto Griggio
,
Thi Thieu Hoa Le
,
Roberto Sebastiani
Journal:
Computing Research Repository  CORR
, vol. abs/1010.4, pp. 143157, 2011
Interpolating QuantifierFree Presburger Arithmetic
(
Citations: 1
)
Daniel Kroening
,
Jérôme Leroux
,
Philipp Rümmer
Conference:
Logic Programming and Automated Reasoning/Russian Conference on Logic Programming  LPAR(RCLP)
, pp. 489503, 2010
Beyond QuantifierFree Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)
Angelo Brillout
,
Daniel Kroening
,
Philipp Ruemmer
,
Thomas Wahl
Journal:
Computing Research Repository  CORR
, vol. abs/1011.1, 2010
Automatic inference of abstract type behavior
Mihai Balint
Conference:
Automated Software Engineering  ASE
, pp. 499504, 2010