Reasoning in the theory of heap: satisfiability and interpolation
From MaRDI portal
Publication:2119112
DOI10.1007/978-3-030-68446-4_9OpenAlexW3132258587MaRDI QIDQ2119112
Publication date: 23 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-68446-4_9
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Cell morphing: from array programs to array-free Horn clauses
- Efficient interpolation for the theory of arrays
- A decision procedure for (co)datatypes in SMT solvers
- Quantifier-Free Interpolation of a Theory of Arrays
- Horn Clause Solvers for Program Verification
- Weakly Equivalent Arrays
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Program Verification using Constraint Handling Rules and Array Constraint Generalizations*
- Quantified Heap Invariants for Object-Oriented Programs
- Low-level liquid types
- Decision procedures for algebraic data types with abstractions
- Tools and Algorithms for the Construction and Analysis of Systems
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Complete instantiation-based interpolation
This page was built for publication: Reasoning in the theory of heap: satisfiability and interpolation
