Specifying and reasoning about shared-variable concurrency

DOI10.1007/978-3-031-40436-8_5MaRDI QIDQ6535828zbMATH OpenFDO

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

Publication date 28 February 2024

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)

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

Cites work

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