Precision and the Conjunction Rule in Concurrent Separation Logic

DOI10.1016/j.entcs.2011.09.021zbMath1342.68085OpenAlexW2157109596WikidataQ113318225 ScholiaQ113318225MaRDI QIDQ5739357

Alexey Gotsman, Byron Cook, Josh Berdine

Publication date: 15 July 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2011.09.021

zbMATH Keywords

precisionconcurrencyseparation logicconjunction rule

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Bringing Order to the Separation Logic Jungle ⋮ Concurrent Separation Logic and Operational Semantics ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra

Cites Work

• Unnamed Item
• A semantics for concurrent separation logic
• Resources, concurrency, and local reasoning
• Goto statements: Semantics and deduction systems
• Scalable Shape Analysis for Systems Code
• Independence and concurrent separation logic
• Modular verification of preemptive OS kernels
• Systematic design of program transformation frameworks by abstract interpretation
• Permission accounting in separation logic

This page was built for publication: Precision and the Conjunction Rule in Concurrent Separation Logic