Complete instantiation-based interpolation
From MaRDI portal
Publication:5890659
DOI10.1007/s10817-016-9371-7zbMath1356.68203OpenAlexW2342179682MaRDI QIDQ5890659
Publication date: 25 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.295.8370
Craig interpolationamalgamationprogram verificationsatisfiability modulo theorieslocal theory extensions
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Interpolation, preservation, definability (03C40)
Related Items
Modularity results for interpolation, amalgamation and superamalgamation ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ On Interpolation and Symbol Elimination in Theory Extensions ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Reasoning in the theory of heap: satisfiability and interpolation
Uses Software
Cites Work
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Amalgamation properties and interpolation theorems for equational theories
- An interpolating theorem prover
- Lazy Abstraction with Interpolants for Arrays
- From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- Back to the future
- Universal relational systems
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Abstractions from proofs
- Ground Interpolation for the Theory of Equality
- Interpolation in local theory extensions
- Error Invariants
- Ground Interpolation for Combined Theories
- An Efficient Decision Procedure for Imperative Tree Data Structures
- Counterexample-guided focus
- Nested interpolants
- Proof Tree Preserving Interpolation
- Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Constraint Solving for Interpolation
- Interpolant-Based Transition Relation Approximation
- On Local Reasoning in Verification
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- On Hierarchical Reasoning in Combinations of Theories
- Interpolation and Symbol Elimination in Vampire
- Lazy Abstraction with Interpolants
- Complete instantiation-based interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Computer Aided Verification
