Balancing expressiveness in formal approaches to concurrency
From MaRDI portal
Publication:890478
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
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
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
