Foundations for decision problems in separation logic with general inductive predicates
From MaRDI portal
Recommendations
- A decision procedure for satisfiability in separation logic with inductive predicates
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Deciding entailments in inductive separation logic with tree automata
- Tractability of separation logic with inductive definitions: beyond lists
- Tractable Reasoning in a Fragment of Separation Logic
Cited in
(28)- Unifying decidable entailments in separation logic with inductive definitions
- Separation logic with linearly compositional inductive predicates and set data constraints
- Strong-separation logic
- Separation logic with one quantified variable
- A complete decision procedure for linearly compositional separation logic with data constraints
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Disproving inductive entailments in separation logic via base pair approximation
- Deciding entailments in inductive separation logic with tree automata
- Separation logic with monadic inductive definitions and implicit existentials
- Separation logics and modalities: a survey
- Decidability for entailments of symbolic heaps with arrays
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- Extending propositional separation logic for robustness properties
- Tractability of separation logic with inductive definitions: beyond lists
- Expressive completeness of separation logic with two variables and no separating conjunction
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Program Verification with Separation Logic
- An efficient cyclic entailment procedure in a fragment of separation logic
- An undecidability result for separation logic with theory reasoning
- Foundations for entailment checking in quantitative separation logic
- Completeness of cyclic proofs for symbolic heaps with inductive definitions
- Restriction on cut rule in cyclic-proof system for symbolic heaps
- Decidable entailments in separation logic with inductive definitions: beyond establishment
- Representation of Peano arithmetic in separation logic
- Beyond symbolic heaps: deciding separation logic with inductive definitions
- Entailment checking in separation logic with inductive definitions is 2-ExpTime hard
- Encoding Peano arithmetic in a minimal fragment of separation logic
This page was built for publication: Foundations for decision problems in separation logic with general inductive predicates
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5410687)
