The Rely-Guarantee method for verifying shared variable concurrent programs
From MaRDI portal
(Redirected from Publication:1362776)
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
(38)- A coinductive calculus for asynchronous side-effecting processes
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- scientific article; zbMATH DE number 1956564 (Why is no real title available?)
- Axiomatic semantics of projection temporal logic programs
- Compositional verification of a communication protocol for a remotely operated aircraft
- A rely-guarantee-based simulation for verifying concurrent program transformations
- Flashix: modular verification of a concurrent and crash-safe flash file system
- scientific article; zbMATH DE number 3938541 (Why is no real title available?)
- Program equivalence in linear contexts
- Trace-based derivation of a scalable lock-free stack algorithm
- Automatic Synthesis of Assumptions for Compositional Model Checking
- Compositional reasoning using the assumption-commitment paradigm
- Lazy compositional verication
- The need for compositional proof systems: a survey
- A Structural Proof of the Soundness of Rely/guarantee Rules
- Observation-based concurrent program logic for relaxed memory consistency models
- A calculus of atomic actions
- On rely-guarantee reasoning
- scientific article; zbMATH DE number 6774232 (Why is no real title available?)
- Compositionality Entails Sequentializability
- scientific article; zbMATH DE number 1487492 (Why is no real title available?)
- Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
- Explicit stabilisation for modular rely-guarantee reasoning
- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
- Tournaments for mutual exclusion: verification and concurrent complexity
- Compositional reasoning for shared-variable concurrent programs
- A Bibliography of Willem-Paul de Roever
- Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics
- CSimpl: a rely-guarantee-based framework for verifying concurrent programs
- Probabilistic rely-guarantee calculus
- 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
- Compositional reasoning for non-multicopy atomic architectures
- Jifeng He at Oxford and beyond: an appreciation
- Modular verification for shared-variable concurrent programs
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)
