Tractable Reasoning in a Fragment of Separation Logic

DOI10.1007/978-3-642-23217-6_16zbMath1300.03017OpenAlexW135237429MaRDI QIDQ3090833

Byron Cook, Christoph Haase, Matthew J. Parkinson, Joël Ouaknine, James Worrell

Publication date: 2 September 2011

Published in: CONCUR 2011 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-23217-6_16

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70)

Related Items (22)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ A First-Order Logic with Frames ⋮ Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ Disproving Inductive Entailments in Separation Logic via Base Pair Approximation ⋮ Separation logic with one quantified variable ⋮ 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 ⋮ On the almighty wand ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Strong-separation logic ⋮ Unnamed Item ⋮ Unifying separation logic and region logic to allow interoperability ⋮ Unnamed Item ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints ⋮ Tractable Reasoning in a Fragment of Separation Logic ⋮ On Symbolic Heaps Modulo Permission Theories ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

Uses Software

• VeriFast
• Smallfoot
• jStar

Cites Work

• Tractable Reasoning in a Fragment of Separation Logic
• BI as an assertion language for mutable data structures
• Shape Analysis for Composite Data Structures
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Containment and equivalence for a fragment of XPath
• Unnamed Item
• Unnamed Item

This page was built for publication: Tractable Reasoning in a Fragment of Separation Logic