On rely-guarantee reasoning

DOI10.1007/978-3-319-19797-5_2MaRDI QIDQ2941165zbMATH OpenOpenAlexFDO

Authors 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

concurrencyrely-guaranteesemanticssoundness

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)

Recommendations

• Generalised rely-guarantee concurrency: an algebraic foundation
• A Structural Proof of the Soundness of Rely/guarantee Rules
• scientific article; zbMATH DE number 1956564
• scientific article; zbMATH DE number 3938541
• Deny-Guarantee Reasoning

Cites work

• A generalization of Owicki-Gries's Hoare logic for a concurrent while language
• A refinement calculus for shared-variable parallel and distributed programming
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Balancing expressiveness in formal approaches to concurrency
• Concurrency verification. Introduction to compositional and noncompositional methods
• Concurrent Kleene Algebra
• Constructing the views framework
• Explicit stabilisation for modular rely-guarantee reasoning
• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• The Rely-Guarantee method for verifying shared variable concurrent programs
• The specification statement
• Views, compositional reasoning for concurrent programs

Cited in

(15)

• Towards a formal treatment of implicit invocation using rely/guarantee reasoning
• An abstract contract theory for programs with procedures
• Observation-based concurrent program logic for relaxed memory consistency models
• Generalised rely-guarantee concurrency: an algebraic foundation
• A Marriage of Rely/Guarantee and Separation Logic
• Explicit stabilisation for modular rely-guarantee reasoning
• Deny-Guarantee Reasoning
• scientific article; zbMATH DE number 3938541 (Why is no real title available?)
• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• Probabilistic rely-guarantee calculus
• Local rely-guarantee reasoning
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Rely-guarantee reasoning for causally consistent shared memory
• A parametric rely-guarantee reasoning framework for concurrent reactive systems
• ConcurrentHOL

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: On rely-guarantee reasoning

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