Generalised rely-guarantee concurrency: an algebraic foundation

DOI10.1007/s00165-016-0384-0zbMath1348.68035arXiv1603.01776OpenAlexW2293609693MaRDI QIDQ333330

Ian J. Hayes

Publication date: 28 October 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1603.01776

zbMATH Keywords

concurrent programmingprogram verificationconcurrent Kleene algebraprogram algebrarely-guarantee concurrency

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

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 ⋮ Unifying theories of reactive design contracts ⋮ Encoding fairness in a synchronous concurrent program algebra ⋮ Automated verification of reactive and concurrent programs by calculation

Cites Work

• Concurrent Kleene algebra and its foundations
• A theoretical basis for stepwise refinement and the programming calculus
• Balancing expressiveness in formal approaches to concurrency
• On correct refinement of programs
• Reasoning algebraically about loops
• A refinement calculus for shared-variable parallel and distributed programming
• Algebraic and coalgebraic methods in the mathematics of program construction. International summer school and workshop, Oxford, GB, April 10--14, 2000. Revised lectures
• Towards a refinement algebra
• Tentative steps toward a development method for interfering programs
• Laws of programming
• Refinement Calculus
• The specification statement
• A Structural Proof of the Soundness of Rely/guarantee Rules
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item