Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
From MaRDI portal
Recommendations
- A decision procedure for satisfiability in separation logic with inductive predicates
- Foundations for decision problems in separation logic with general inductive predicates
- A proof procedure for separation logic with inductive definitions and data
- A decision procedure for separation logic in SMT
- A decidable fragment in separation logic with inductive predicates and arithmetic
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Unifying decidable entailments in separation logic with inductive definitions
- Tractability of separation logic with inductive definitions: beyond lists
- Deciding entailments in inductive separation logic with tree automata
- scientific article; zbMATH DE number 1639660
Cites work
- A decision procedure for satisfiability in separation logic with inductive predicates
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Deciding entailments in inductive separation logic with tree automata
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Model checking for symbolic-heap separation logic with inductive predicates
- Programming Languages and Systems
- Quantitative separation logic and programs with lists
- Separation logic modulo theories
- The tree width of separation logic with recursive definitions
Cited in
(16)- Unifying decidable entailments in separation logic with inductive definitions
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Separation logic with linearly compositional inductive predicates and set data constraints
- Compositional satisfiability solving in separation logic
- Enhancing symbolic execution of heap-based programs with separation logic for test input generation
- Separation logic with monadic inductive definitions and implicit existentials
- Satisfiability modulo heap-based programs
- A decision procedure for satisfiability in separation logic with inductive predicates
- Decidability for entailments of symbolic heaps with arrays
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- Tractability of separation logic with inductive definitions: beyond lists
- Certified reasoning with infinity
- Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
- Effective entailment checking for separation logic with inductive definitions
- Representation of Peano arithmetic in separation logic
- Encoding Peano arithmetic in a minimal fragment of separation logic
This page was built for publication: Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179308)
