Complete instantiation-based interpolation
From MaRDI portal
Recommendations
- Complete instantiation-based interpolation
- scientific article; zbMATH DE number 3914875
- Universal interpolation
- Interpolation in practical formal development
- scientific article; zbMATH DE number 4109278
- Towards a general interpolation scheme
- Interpolation through an iterative scheme
- A recursive method for computing interpolants
- Complete parameterization of piecewise-polynomial interpolation kernels
- Interpolation
Cites work
- Abstractions from proofs
- Amalgamation properties and interpolation theorems for equational theories
- An efficient decision procedure for imperative tree data structures
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- An interpolating theorem prover
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Back to the future, revisiting precise program verification using SMT solvers
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- Complete instantiation-based interpolation
- Constraint Solving for Interpolation
- Counterexample-guided focus
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Error invariants
- From strong amalgamability to modularity of quantifier-free interpolation
- Ground Interpolation for Combined Theories
- Ground Interpolation for the Theory of Equality
- Interpolant-Based Transition Relation Approximation
- Interpolation and SAT-based model checking.
- Interpolation and symbol elimination in Vampire
- Interpolation in local theory extensions
- Lazy Abstraction with Interpolants
- Lazy abstraction with interpolants for arrays
- Nested interpolants
- On Hierarchical Reasoning in Combinations of Theories
- On Local Reasoning in Verification
- Proof tree preserving interpolation
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Rewriting-based quantifier-free interpolation for a theory of arrays
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Universal relational systems
Cited in
(14)- Efficient interpolation for the theory of arrays
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Reasoning in the theory of heap: satisfiability and interpolation
- Interpolation and amalgamation for arrays with MaxDiff
- Modularity results for interpolation, amalgamation and superamalgamation
- Interpolation in practical formal development
- Spatial interpolants
- On interpolation in decision procedures
- An extension of lazy abstraction with interpolation for programs with arrays
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Complete instantiation-based interpolation
- Interpolation Results for Arrays with Length and MaxDiff
- Interpolating parametric array theories
- On recursion-free Horn clauses and Craig interpolation
This page was built for publication: Complete instantiation-based interpolation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5890659)
