On Rely-Guarantee Reasoning

DOI10.1007/978-3-319-19797-5_2zbMath1432.68321OpenAlexW1189894384MaRDI QIDQ2941165

Stephan van Staden

Publication date: 27 August 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-19797-5_2

zbMATH Keywords

semanticsconcurrencysoundnessrely-guarantee

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models ⋮ An abstract contract theory for programs with procedures

Uses Software

• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Balancing expressiveness in formal approaches to concurrency
• A generalization of Owicki-Gries's Hoare logic for a concurrent while language
• The Rely-Guarantee method for verifying shared variable concurrent programs
• A refinement calculus for shared-variable parallel and distributed programming
• Constructing the Views Framework
• Views
• Concurrent Kleene Algebra
• Explicit Stabilisation for Modular Rely-Guarantee Reasoning
• The specification statement
• A Structural Proof of the Soundness of Rely/guarantee Rules

This page was built for publication: On Rely-Guarantee Reasoning