Separation logic and concurrency

DOI10.1007/978-1-84882-736-3_7MaRDI QIDQ3557673zbMATH OpenOpenAlexFDO

Authors Richard Bornat

Publication date 23 April 2010

Published in Formal Methods: State of the Art and New Directions (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-1-84882-736-3_7

zbMATH Keywords

Hoare logic

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• CONCUR 2004 - Concurrency Theory
• A semantics for concurrent separation logic
• Fine-grained concurrency with separation logic
• Concurrent separation logic and operational semantics
• A revisionist history of concurrent separation logic

Cited in

(38)

• Separating systems of conjunctions.
• A game semantics of concurrent separation logic
• Reasoning over permissions regions in concurrent separation logic
• Logical reasoning for disjoint permissions
• scientific article; zbMATH DE number 1670481 (Why is no real title available?)
• Certificates and Separation Logic
• Barriers in concurrent separation logic: now with tool support!
• Fictional separation logic
• Syntactic control of interference for separation logic
• Temporary read-only permissions for separation logic
• Barriers in Concurrent Separation Logic
• Permission-based separation logic for message-passing concurrency
• The ``Hoare Logic of CSP, and All That
• Independence and concurrent separation logic
• Formal verification of concurrent programs with Read-write locks
• Parameterized Memory Models and Concurrent Separation Logic
• Reasoning about optimistic concurrency using a program logic for history
• Separation Logic for Higher-Order Store
• Automatic Parallelization with Separation Logic
• Reasoning About Data-Parallel Pointer Programs in a Modal Extension of Separation Logic
• Concurrent separation logic for pipelined parallelization
• Expressing the behavior of three very different concurrent systems by using natural extensions of separation logic
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Reasoning about separation using abstraction and reification
• Permission accounting in separation logic
• Convolution as a Unifying Concept
• CONCUR 2004 - Concurrency Theory
• Modular reasoning about separation of concurrent data structures
• A separation logic for refining concurrent objects
• Separation Logic Semantics for Communicating Processes
• Separation Logic for Multiple Inheritance
• Programming Languages and Systems
• Separation Logic Tutorial
• Separation Logic Contracts for a Java-Like Language with Fork/Join
• Concurrent separation logic and operational semantics
• Inter-process buffers in separation logic with rely-guarantee
• Fine-grained concurrency with separation logic
• A semantics for concurrent separation logic

This page was built for publication: Separation logic and concurrency

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