Balancing expressiveness in formal approaches to concurrency

DOI10.1007/s00165-014-0310-2zbMath1343.68171OpenAlexW2219157221WikidataQ59409981 ScholiaQ59409981MaRDI QIDQ890478

Ian J. Hayes, Cliff B. Jones, Robert J. Colvin

Publication date: 10 November 2015

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

Full work available at URL: https://doi.org/10.1007/s00165-014-0310-2

zbMATH Keywords

concurrencyseparation logicrely/guarantee reasoning

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Modelling and analysing neural networks using a hybrid process algebra ⋮ Possible values: exploring a concept for concurrency ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ An application of temporal projection to interleaving concurrency ⋮ 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 ⋮ Guest editors' preface to special issue on interval temporal logics ⋮ Reasoning about Separation Using Abstraction and Reification

Uses Software

• Line-up

Cites Work

• Explanation of two non-blocking shared-variable communication algorithms
• Elucidating concurrent algorithms via layers of abstraction and reification
• Concurrent Kleene algebra and its foundations
• A theoretical basis for stepwise refinement and the programming calculus
• Inter-process buffers in separation logic with rely-guarantee
• Splitting atoms safely
• Resources, concurrency, and local reasoning
• An axiomatic proof technique for parallel programs
• A refinement calculus for shared-variable parallel and distributed programming
• Towards a refinement algebra
• Concurrent Library Correctness on the TSO Memory Model
• Views
• Liveness-Preserving Atomicity Abstraction
• The Role of Auxiliary Variables in the Formal Development of Concurrent Programs
• A Marriage of Rely/Guarantee and Separation Logic
• Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
• Modular Safety Checking for Fine-Grained Concurrency
• Deny-Guarantee Reasoning
• Tentative steps toward a development method for interfering programs
• The B-Book
• Refinement Calculus
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• Proving that non-blocking algorithms don't block
• Local rely-guarantee reasoning
• Impredicative Concurrent Abstract Predicates
• A Structural Proof of the Soundness of Rely/guarantee Rules
• The next 700 programming languages
• An axiomatic basis for computer programming
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item