The Rely-Guarantee method for verifying shared variable concurrent programs
From MaRDI portal
Publication:1362776
DOI10.1007/BF01211617zbMath0874.68202MaRDI QIDQ1362776
Jifeng He, Qiwen Xu, Willem Paul de Roever
Publication date: 10 November 1997
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Related Items
Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models ⋮ On Rely-Guarantee Reasoning ⋮ Tournaments for mutual exclusion: verification and concurrent complexity ⋮ A coinductive calculus for asynchronous side-effecting processes ⋮ Jifeng He at Oxford and beyond: an appreciation ⋮ Compositional verification of a communication protocol for a remotely operated aircraft ⋮ Compositionality Entails Sequentializability ⋮ CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ A Bibliography of Willem-Paul de Roever ⋮ Compositional reasoning for shared-variable concurrent programs ⋮ Axiomatic semantics of projection temporal logic programs ⋮ Automatic Synthesis of Assumptions for Compositional Model Checking ⋮ 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 ⋮ Program equivalence in linear contexts ⋮ Flashix: modular verification of a concurrent and crash-safe flash file system
Cites Work
- A generalization of Owicki-Gries's Hoare logic for a concurrent while language
- Recursive assertions and parallel programs
- Proving total correctness of nondeterministic programs in infinitary logic
- An axiomatic proof technique for parallel programs
- Full abstraction for a shared-variable parallel language
- Proofs of Networks of Processes
- Soundness and Completeness of an Axiom System for Program Verification
