The Rely-Guarantee method for verifying shared variable concurrent programs
From MaRDI portal
Recommendations
Cites work
- A generalization of Owicki-Gries's Hoare logic for a concurrent while language
- An axiomatic proof technique for parallel programs
- Full abstraction for a shared-variable parallel language
- Proofs of Networks of Processes
- Proving total correctness of nondeterministic programs in infinitary logic
- Recursive assertions and parallel programs
- Soundness and Completeness of an Axiom System for Program Verification
Cited in
(34)- Trace-based derivation of a scalable lock-free stack algorithm
- Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
- scientific article; zbMATH DE number 6774232 (Why is no real title available?)
- CSimpl: a rely-guarantee-based framework for verifying concurrent programs
- Compositional reasoning for non-multicopy atomic architectures
- A coinductive calculus for asynchronous side-effecting processes
- A calculus of atomic actions
- Flashix: modular verification of a concurrent and crash-safe flash file system
- Explicit stabilisation for modular rely-guarantee reasoning
- scientific article; zbMATH DE number 1956564 (Why is no real title available?)
- scientific article; zbMATH DE number 3938541 (Why is no real title available?)
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- A Bibliography of Willem-Paul de Roever
- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
- Program equivalence in linear contexts
- Axiomatic semantics of projection temporal logic programs
- Assume-guarantee reasoning for additive hybrid behaviour
- A parametric rely-guarantee reasoning framework for concurrent reactive systems
- Rely-guarantee reasoning for causally consistent shared memory
- Specifying and reasoning about shared-variable concurrency
- A rely-guarantee-based simulation for verifying concurrent program transformations
- On rely-guarantee reasoning
- Observation-based concurrent program logic for relaxed memory consistency models
- Tournaments for mutual exclusion: verification and concurrent complexity
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Compositional reasoning for shared-variable concurrent programs
- Modular verification for shared-variable concurrent programs
- Automatic Synthesis of Assumptions for Compositional Model Checking
- Probabilistic rely-guarantee calculus
- scientific article; zbMATH DE number 1487492 (Why is no real title available?)
- Compositional verification of a communication protocol for a remotely operated aircraft
- Jifeng He at Oxford and beyond: an appreciation
- Compositionality Entails Sequentializability
- A Structural Proof of the Soundness of Rely/guarantee Rules
This page was built for publication: The Rely-Guarantee method for verifying shared variable concurrent programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1362776)
