Inter-process buffers in separation logic with rely-guarantee

DOI10.1007/s00165-009-0141-8zbMath1214.68131OpenAlexW2142118968WikidataQ130880073 ScholiaQ130880073MaRDI QIDQ613139

Hasan Amjad, Richard Bornat

Publication date: 17 December 2010

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-009-0141-8

zbMATH Keywords

concurrencyseparation logicrely-guarantee

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 (6)

Possible values: exploring a concept for concurrency ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification ⋮ Explanation of two non-blocking shared-variable communication algorithms ⋮ Elucidating concurrent algorithms via layers of abstraction and reification

Uses Software

• SPARK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantics for concurrent separation logic
• Resources, concurrency, and local reasoning
• Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
• Proving pointer programs in higher-order logic
• Modular verification of a non-blocking stack
• A Marriage of Rely/Guarantee and Separation Logic
• Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
• Towards Automatic Stability Analysis for Rely-Guarantee Proofs
• Modular Safety Checking for Fine-Grained Concurrency
• Verifying properties of parallel programs
• The Logic of Bunched Implications
• Randomized wait-free concurrent objects (extended abstract)
• Permission accounting in separation logic
• An axiomatic basis for computer programming

This page was built for publication: Inter-process buffers in separation logic with rely-guarantee