Balancing expressiveness in formal approaches to concurrency
type: Item
instance of: scholarly article
title: Balancing expressiveness in formal approaches to concurrency
zbMATH Open document ID: 1343.68171
author: Cliff B. Jones
author: Ian Hayes
author: Robert Colvin
published in: Formal Aspects of Computing
publication date: 2015-11-10T00:00:00Z
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 6506757
zbMATH Keywords: concurrency
zbMATH Keywords: rely/guarantee reasoning
zbMATH Keywords: separation logic
Wikidata QID: Q59409981
describes a project that uses: Line-up
MaRDI profile type: Publication
full work available at URL: s00165-014-0310-2
OpenAlex ID: W2219157221
cites work: The B-Book
cites work: Q3569584
cites work: Q5679697
cites work: An axiomatic proof technique for parallel programs
cites work: Inter-process buffers in separation logic with rely-guarantee
cites work: Explanation of two non-blocking shared-variable communication algorithms
cites work: Concurrent Library Correctness on the TSO Memory Model
cites work: Q4813391
cites work: Refinement Calculus
cites work: The next 700 programming languages
cites work: A Structural Proof of the Soundness of Rely/guarantee Rules
cites work: Q5684216
cites work: Deny-Guarantee Reasoning
cites work: Q4471919
cites work: A refinement calculus for shared-variable parallel and distributed programming
cites work: Concurrency verification. Introduction to compositional and noncompositional methods
cites work: Splitting atoms safely
cites work: Views
cites work: Local rely-guarantee reasoning
cites work: On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
cites work: Q5584402
cites work: Proving that non-blocking algorithms don't block
cites work: Liveness-Preserving Atomicity Abstraction
cites work: Elucidating concurrent algorithms via layers of abstraction and reification
cites work: Concurrent Kleene algebra and its foundations
cites work: An axiomatic basis for computer programming
cites work: Q3859249
cites work: Tentative steps toward a development method for interfering programs
cites work: Q3997074
cites work: The Role of Auxiliary Variables in the Formal Development of Concurrent Programs
cites work: Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
cites work: A theoretical basis for stepwise refinement and the programming calculus
cites work: Q4301161
cites work: Q3680239
cites work: Resources, concurrency, and local reasoning
cites work: Q4178461
cites work: Q4417904
cites work: Impredicative Concurrent Abstract Predicates
cites work: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
cites work: Modular Safety Checking for Fine-Grained Concurrency
cites work: A Marriage of Rely/Guarantee and Separation Logic
cites work: Towards a refinement algebra
DOI: 10.1007/S00165-014-0310-2
description: scientific article; zbMATH DE number 6506757