Specifying and reasoning about shared-variable concurrency

DOI10.1007/978-3-031-40436-8_5zbMATH Open1547.685MaRDI QIDQ6535828FDOQ6535828

Authors: Ian Hayes, Cliff B. Jones, Larissa A. Meinicke 

Publication date: 28 February 2024

Recommendations

• The Rely-Guarantee method for verifying shared variable concurrent programs
• Modular verification for shared-variable concurrent programs
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• scientific article; zbMATH DE number 3956417
• Elucidating concurrent algorithms via layers of abstraction and reification

zbMATH Keywords

refinement calculusprogram algebrashared-variable concurrencyatomic specification commandsrely-guarantee approach

Mathematics Subject Classification ID

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

Cites Work

• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Laws of programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Title not available (Why is that?)
• Resources, concurrency, and local reasoning
• An axiomatic proof technique for parallel programs
• Concurrent Kleene Algebra
• The specification statement
• Algebras for program correctness in Isabelle/HOL
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Concurrent Kleene algebra and its foundations
• A refinement calculus for shared-variable parallel and distributed programming
• Generalised rely-guarantee concurrency: an algebraic foundation
• Tentative steps toward a development method for interfering programs
• A Marriage of Rely/Guarantee and Separation Logic
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
• Splitting atoms safely
• The Rely-Guarantee method for verifying shared variable concurrent programs
• Title not available (Why is that?)
• Proving assertions about parallel programs
• Modular Safety Checking for Fine-Grained Concurrency
• Explanation of two non-blocking shared-variable communication algorithms
• Inter-process buffers in separation logic with rely-guarantee
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Shared Memory Computer Display System
• Encoding fairness in a synchronous concurrent program algebra
• A program logic for concurrent objects under fair scheduling
• Title not available (Why is that?)
• Title not available (Why is that?)
• Deny-Guarantee Reasoning
• Local rely-guarantee reasoning
• Designing a semantic model for a wide-spectrum language with concurrency
• Fifty years of Hoare's logic
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
• Possible values: exploring a concept for concurrency
• Reasoning about separation using abstraction and reification
• Explicit stabilisation for modular rely-guarantee reasoning
• Towards a thread-local proof technique for starvation freedom

This page was built for publication: Specifying and reasoning about shared-variable concurrency

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