A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency

DOI10.1007/s00165-018-0464-4zbMath1425.68293arXiv1710.03352OpenAlexW2964284238WikidataQ129416433 ScholiaQ129416433MaRDI QIDQ2414249

Kirsten Winter, Robert J. Colvin, Larissa A. Meinicke, Ian J. Hayes

Publication date: 10 May 2019

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

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

zbMATH Keywords

process algebrarefinement calculusconcurrencyprogram algebrarely/guaranteesynchronous parallel

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Encoding fairness in a synchronous concurrent program algebra

Uses Software

• Isabelle/HOL
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Generalised rely-guarantee concurrency: an algebraic foundation
• Concurrent Kleene algebra and its foundations
• A theoretical basis for stepwise refinement and the programming calculus
• A single complete rule for data refinement
• Synchronous Kleene algebra
• Balancing expressiveness in formal approaches to concurrency
• Calculi for synchrony and asynchrony
• A calculus of communicating systems
• On correct refinement of programs
• An axiomatic proof technique for parallel programs
• Isabelle/HOL. A proof assistant for higher-order logic
• Designing a semantic model for a wide-spectrum language with concurrency
• Towards a refinement algebra
• An algebra of synchronous atomic steps
• Possible values: exploring a concept for concurrency
• CSP with Hierarchical State
• Tentative steps toward a development method for interfering programs
• Process algebra for synchronous communication
• Refinement Calculus
• The specification statement
• Algebras for Program Correctness in Isabelle/HOL
• A Structural Proof of the Soundness of Rely/guarantee Rules

This page was built for publication: A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency