Tractable Reasoning in a Fragment of Separation Logic
From MaRDI portal
Recommendations
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- A separation logic for a promising semantics
- Separation logic style reasoning in a refinement based language
- A decidable fragment in separation logic with inductive predicates and arithmetic
- An undecidability result for separation logic with theory reasoning
- Tractable reasoning using logic programs with intensional concepts
- Compositional entailment checking for a fragment of separation logic
- Compositional entailment checking for a fragment of separation logic
- An efficient cyclic entailment procedure in a fragment of separation logic
Cites work
- BI as an assertion language for mutable data structures
- Containment and equivalence for a fragment of XPath
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- scientific article; zbMATH DE number 3639144 (Why is no real title available?)
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- Shape Analysis for Composite Data Structures
- Tractable Reasoning in a Fragment of Separation Logic
Cited in
(36)- Compositional entailment checking for a fragment of separation logic
- Unifying separation logic and region logic to allow interoperability
- A separation logic with data: small models and automation
- Tractable reasoning in artificial intelligence
- Tractable reasoning using logic programs with intensional concepts
- Strong-separation logic
- Separation logic with one quantified variable
- A complete decision procedure for linearly compositional separation logic with data constraints
- Two-Variable Separation Logic and Its Inner Circle
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Tractable Reasoning in a Fragment of Separation Logic
- Disproving inductive entailments in separation logic via base pair approximation
- On the almighty wand
- Separation logics and modalities: a survey
- Decidability for entailments of symbolic heaps with arrays
- A first-order logic with frames
- 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
- On Symbolic Heaps Modulo Permission Theories
- Expressive completeness of separation logic with two variables and no separating conjunction
- 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
- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
- A proof procedure for separation logic with inductive definitions and data
- An efficient cyclic entailment procedure in a fragment of separation logic
- On the complexity of pointer arithmetic in separation logic
- 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
- Representation of Peano arithmetic in separation logic
- Tractable and intractable entailment problems in separation logic with inductively defined predicates
- Expressiveness results for an inductive logic of separated relations
- Beyond symbolic heaps: deciding separation logic with inductive definitions
- An EXPTIME-complete entailment problem in separation logic
- Encoding Peano arithmetic in a minimal fragment of separation logic
This page was built for publication: Tractable Reasoning in a Fragment of Separation Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3090833)
