The Tree Width of Separation Logic with Recursive Definitions
From MaRDI portal
Publication:4928426
DOI10.1007/978-3-642-38574-2_2zbMath1329.03068arXiv1301.5139OpenAlexW1910824881MaRDI QIDQ4928426
Adam Rogalewicz, Radu Iosif, Jiří Šimáček
Publication date: 14 June 2013
Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1301.5139
Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Data structures (68P05)
Related Items
Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ Disproving Inductive Entailments in Separation Logic via Base Pair Approximation ⋮ Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic ⋮ Separation logic with one quantified variable ⋮ Automated mutual induction proof in separation logic ⋮ Separation logics and modalities: a survey ⋮ Unnamed Item ⋮ A proof procedure for separation logic with inductive definitions and data ⋮ Compositional entailment checking for a fragment of separation logic ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Two-Variable Separation Logic and Its Inner Circle ⋮ An undecidability result for separation logic with theory reasoning ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ Nested antichains for WS1S ⋮ Strong-separation logic ⋮ Lazy Automata Techniques for WS1S ⋮ Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules ⋮ Unnamed Item ⋮ Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps ⋮ Unnamed Item ⋮ On Temporal and Separation Logics ⋮ Juggrnaut: using graph grammars for abstracting unbounded heap structures ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints ⋮ Unifying decidable entailments in separation logic with inductive definitions ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
Uses Software
