A Structural Proof of the Soundness of Rely/guarantee Rules

DOI10.1093/logcom/exm030zbMath1125.68039OpenAlexW2048467032MaRDI QIDQ5427260

Joey W. Coleman, Cliff B. Jones

Publication date: 19 November 2007

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/3fb23b8bd9f191cd41fcea08dcacc8b48417a3f3

zbMATH Keywords

structural operational semanticsconcurrencysoundnessstructural inductionrely/guarantee reasoning

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (13)

Developments in concurrent Kleene algebra ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ On Rely-Guarantee Reasoning ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Designing a semantic model for a wide-spectrum language with concurrency ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs ⋮ Probabilistic rely-guarantee calculus ⋮ An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Elucidating concurrent algorithms via layers of abstraction and reification ⋮ An operational semantics for object-oriented concepts based on the class hierarchy

This page was built for publication: A Structural Proof of the Soundness of Rely/guarantee Rules