Tractable Reasoning in a Fragment of Separation Logic

DOI10.1007/978-3-642-23217-6_16zbMath1300.03017MaRDI 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

68Q25: Analysis of algorithms and problem complexity

03B70: Logic in computer science

Related Items

Separation logics and modalities: a survey, Unnamed Item, Unnamed Item, Unnamed Item, Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction, On the almighty wand, Compositional entailment checking for a fragment of separation logic, Unifying separation logic and region logic to allow interoperability, 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, Tractable Reasoning in a Fragment of Separation Logic, Disproving Inductive Entailments in Separation Logic via Base Pair Approximation

Uses Software

• VeriFast
• Smallfoot
• jStar

Cites Work

• Unnamed Item
• Unnamed Item
• 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