The tree width of separation logic with recursive definitions
From MaRDI portal
Abstract: Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to decide satisfiability and validity of entailments for Separation Logic(s) over lists (possibly with data). In this paper we establish a more general decidability result. We prove that any Separation Logic formula using rather general recursively defined predicates is decidable for satisfiability, and moreover, entailments between such formulae are decidable for validity. These predicates are general enough to define (doubly-) linked lists, trees, and structures more general than trees, such as trees whose leaves are chained in a list. The decidability proofs are by reduction to decidability of Monadic Second Order Logic on graphs with bounded tree width.
Recommendations
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Deciding entailments in inductive separation logic with tree automata
- Separation logic with monadic inductive definitions and implicit existentials
- A separation logic with data: small models and automation
- Tractability of separation logic with inductive definitions: beyond lists
Cited in
(50)- Compositional entailment checking for a fragment of separation logic
- Nested antichains for WS1S
- A separation logic with data: small models and automation
- Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
- Unifying decidable entailments in separation logic with inductive definitions
- Strong-separation logic
- Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
- A decidable logic for tree data-structures with measurements
- Separation logic with one quantified variable
- Automated mutual induction proof in separation logic
- A complete decision procedure for linearly compositional separation logic with data constraints
- Two-Variable Separation Logic and Its Inner Circle
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Lazy automata techniques for WS1S
- Disproving inductive entailments in separation logic via base pair approximation
- Separation logic with monadic inductive definitions and implicit existentials
- Tree-like grammars and separation logic
- Beyond Shapes: Lists with Ordered Data
- Separation logics and modalities: a survey
- Decidability for entailments of symbolic heaps with arrays
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- On temporal and separation logics
- 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
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Default logic and bounded treewidth
- A proof procedure for separation logic with inductive definitions and data
- 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
- Testing the satisfiability of formulas in separation logic with permissions
- Restriction on cut rule in cyclic-proof system for symbolic heaps
- Decidable entailments in separation logic with inductive definitions: beyond establishment
- Deciding satisfiability for overlaid symbolic heaps
- Representation of Peano arithmetic in separation logic
- The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
- Tractable and intractable entailment problems in separation logic with inductively defined predicates
- Expressiveness results for an inductive logic of separated relations
- A direct procedure to test entailment in a separation logic of relations
- Beyond symbolic heaps: deciding separation logic with inductive definitions
- Entailment checking in separation logic with inductive definitions is 2-ExpTime hard
- Tree-verifiable graph grammars
- What is decidable in separation logic beyond progress, connectivity and establishment?
- An EXPTIME-complete entailment problem in separation logic
- Encoding Peano arithmetic in a minimal fragment of separation logic
- Juggrnaut: using graph grammars for abstracting unbounded heap structures
This page was built for publication: The tree width of separation logic with recursive definitions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928426)
