Beyond quantifier-free interpolation in extensions of Presburger arithmetic
From MaRDI portal
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.
Recommendations
- Interpolating quantifier-free Presburger arithmetic
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Interpolant based decision procedure for quantifier-free Presburger arithmetic
- Quantifier-free interpolation of a theory of arrays
Cites work
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- An interpolating theorem prover
- Automated Deduction – CADE-20
- Ground Interpolation for the Theory of Equality
- scientific article; zbMATH DE number 837700 (Why is no real title available?)
- Interpolant strength
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Presburger arithmetic with unary predicates is Π11 complete
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Simplify: a theorem prover for program checking
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification, Model Checking, and Abstract Interpretation
Cited in
(19)- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Bounding quantification in parametric expansions of Presburger arithmetic
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Reasoning in the theory of heap: satisfiability and interpolation
- Interpolation systems for ground proofs in automated deduction: a survey
- Quantifier-free interpolation of a theory of arrays
- Guiding Craig interpolation with domain-specific abstractions
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- SAT-Based Model Checking
- Interpolation and model checking
- scientific article; zbMATH DE number 4031630 (Why is no real title available?)
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Interpolating quantifier-free Presburger arithmetic
- Quantifier-free interpolation in combinations of equality interpolating theories
- Interpolant based decision procedure for quantifier-free Presburger arithmetic
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Complete instantiation-based interpolation
- Range-restricted and Horn interpolation through clausal tableaux
- Not all bugs are created equal, but robust reachability can tell the difference
This page was built for publication: Beyond quantifier-free interpolation in extensions of Presburger arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075472)
