Unifying decidable entailments in separation logic with inductive definitions
From MaRDI portal
Recommendations
- Effective entailment checking for separation logic with inductive definitions
- Foundations for decision problems in separation logic with general inductive predicates
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- A decision procedure for satisfiability in separation logic with inductive predicates
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- An undecidability result for separation logic with theory reasoning
- Tractability of separation logic with inductive definitions: beyond lists
- Deciding entailments in inductive separation logic with tree automata
- Separation logic with monadic inductive definitions and implicit existentials
- A proof procedure for separation logic with inductive definitions and data
Cites work
- Automated mutual induction proof in separation logic
- BI as an assertion language for mutable data structures
- Deciding entailments in inductive separation logic with tree automata
- Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
- Foundations for decision problems in separation logic with general inductive predicates
- The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
- The tree width of separation logic with recursive definitions
- Unifying decidable entailments in separation logic with inductive definitions
Cited in
(12)- Unifying decidable entailments in separation logic with inductive definitions
- Decision problems in a logic for reasoning about reconfigurable distributed systems
- Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- 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
- Testing the satisfiability of formulas in separation logic with permissions
- Expressiveness results for an inductive logic of separated relations
- What is decidable in separation logic beyond progress, connectivity and establishment?
- An EXPTIME-complete entailment problem in separation logic
This page was built for publication: Unifying decidable entailments in separation logic with inductive definitions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055854)
