Tractability of separation logic with inductive definitions: beyond lists
From MaRDI portal
Publication:5111651
Recommendations
- Tractable Reasoning in a Fragment of Separation Logic
- Foundations for decision problems in separation logic with general inductive predicates
- The tree width of separation logic with recursive definitions
- A decision procedure for satisfiability in separation logic with inductive predicates
- The effects of adding reachability predicates in propositional separation logic
Cites work
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- A complete decision procedure for linearly compositional separation logic with data constraints
- A decision procedure for satisfiability in separation logic with inductive predicates
- A decision procedure for separation logic in SMT
- Automated cyclic entailment proofs in separation logic
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Biabduction (and related problems) in array separation logic
- Compositional entailment checking for a fragment of separation logic
- Deciding entailments in inductive separation logic with tree automata
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Expressive completeness of separation logic with two variables and no separating conjunction
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Foundations for decision problems in separation logic with general inductive predicates
- Model checking for symbolic-heap separation logic with inductive predicates
- On automated lemma generation for separation logic with inductive definitions
- On the almighty wand
- Programming Languages and Systems
- Satisfiability modulo heap-based programs
- Satisfiability of compositional separation logic with tree predicates and data constraints
- The tree width of separation logic with recursive definitions
- Tractable Reasoning in a Fragment of Separation Logic
Cited in
(8)- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Unifying decidable entailments in separation logic with inductive definitions
- Separation logic with linearly compositional inductive predicates and set data constraints
- The tree width of separation logic with recursive definitions
- The effects of adding reachability predicates in propositional separation logic
- On the complexity of pointer arithmetic in separation logic
- Foundations for decision problems in separation logic with general inductive predicates
- An efficient cyclic entailment procedure in a fragment of separation logic
This page was built for publication: Tractability of separation logic with inductive definitions: beyond lists
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111651)
