On the relation between concurrent separation logic and concurrent Kleene algebra

DOI10.1016/J.JLAMP.2014.08.002MaRDI QIDQ2347904zbMATH OpenOpenAlexWikidataFDO

Authors Peter W. O'Hearn, Rasmus L. Petersen, Jules Villard, Akbar Hussain

Publication date 10 June 2015

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2014.08.002

zbMATH Keywords

compositionalityconcurrencyKleene algebraseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Other algebras related to logic (03G25) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Concurrent Kleene algebra: free model and completeness
• Concurrent Kleene algebra and its foundations
• Concurrent Kleene Algebra
• Revisiting concurrent separation logic
• Foundations of concurrent Kleene algebra

Cites work

• A Basis for Verifying Multi-threaded Programs
• A Marriage of Rely/Guarantee and Separation Logic
• A semantics for concurrent separation logic
• Algebraic and coalgebraic methods in the mathematics of program construction. International summer school and workshop, Oxford, GB, April 10--14, 2000. Revised lectures
• Algebraic separation logic
• An event structure model for probabilistic concurrent Kleene algebra
• BI as an assertion language for mutable data structures
• Concurrent Kleene algebra and its foundations
• Concurrent separation logic and operational semantics
• Deny-Guarantee Reasoning
• Fictional separation logic
• scientific article; zbMATH DE number 3550923 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• In praise of algebra
• Independence and concurrent separation logic
• Laws of programming
• Modular reasoning about separation of concurrent data structures
• Modular Safety Checking for Fine-Grained Concurrency
• On closed categories of functors
• On locality and the exchange law for concurrent processes
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
• Permission accounting in separation logic
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Precision and the conjunction rule in concurrent separation logic
• Reasoning about optimistic concurrency using a program logic for history
• Refinement Calculus
• Resources, concurrency, and local reasoning
• Subjective auxiliary state for coarse-grained concurrency
• The laws of programming unify process calculi
• The Logic of Bunched Implications
• Verifying concurrent memory reclamation algorithms with grace
• Verifying linearizability with hindsight
• Views, compositional reasoning for concurrent programs

Cited in

(12)

• On the concurrent computational content of intermediate logics
• Concurrent Kleene algebra: free model and completeness
• Exploring an interface model for CKA
• A discrete geometric model of concurrent program execution
• On locality and the exchange law for concurrent processes
• Stone-type dualities for separation logics
• scientific article; zbMATH DE number 7204945 (Why is no real title available?)
• Convolution as a Unifying Concept
• Abstract hidden Markov models: a monadic account of quantitative information flow
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
• An algebraic glimpse at bunched implications and separation logic
• Pomsets with boxes: protection, separation, and locality in concurrent Kleene algebra

Describes a project that uses

Uses Software

• VCC

This page was built for publication: On the relation between concurrent separation logic and concurrent Kleene algebra

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2347904)