Inter-process buffers in separation logic with rely-guarantee

DOI10.1007/S00165-009-0141-8MaRDI QIDQ613139zbMATH OpenOpenAlexWikidataFDO

Authors Richard Bornat, Hasan Amjad

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

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

Recommendations

• Explanation of two non-blocking shared-variable communication algorithms
• Separation logic and concurrency
• A Marriage of Rely/Guarantee and Separation Logic
• Barriers in Concurrent Separation Logic
• CONCUR 2004 - Concurrency Theory

Cites work

• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 194003 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 2090146 (Why is no real title available?)
• scientific article; zbMATH DE number 3345157 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• A semantics for concurrent separation logic
• An axiomatic basis for computer programming
• Modular Safety Checking for Fine-Grained Concurrency
• Modular verification of a non-blocking stack
• Permission accounting in separation logic
• Proving pointer programs in higher-order logic
• Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
• Randomized wait-free concurrent objects (extended abstract)
• Resources, concurrency, and local reasoning
• Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
• The Logic of Bunched Implications
• Towards Automatic Stability Analysis for Rely-Guarantee Proofs
• Variables as resource in separation logic
• Verifying properties of parallel programs

Cited in

(8)

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

Describes a project that uses

Uses Software

• SPARK

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

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