The Rely-Guarantee method for verifying shared variable concurrent programs

DOI10.1007/BF01211617zbMATH Open0874.68202MaRDI QIDQ1362776FDOQ1362776

Jifeng He, Willem-Paul de Roever, Qiwen Xu

Publication date: 10 November 1997

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Recommendations

• scientific article; zbMATH DE number 1956564
• scientific article; zbMATH DE number 3938541
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Concurrency verification. Introduction to compositional and noncompositional methods

zbMATH Keywords

rely-guaranteeassumption-commitmentcompositional proof systemsshared variable concurrent programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Full abstraction for a shared-variable parallel language
• Soundness and Completeness of an Axiom System for Program Verification
• An axiomatic proof technique for parallel programs
• Proofs of Networks of Processes
• Proving total correctness of nondeterministic programs in infinitary logic
• A generalization of Owicki-Gries's Hoare logic for a concurrent while language
• Recursive assertions and parallel programs

Cited In (30)

• 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
• Title not available (Why is that?)
• Axiomatic semantics of projection temporal logic programs
• Compositional verification of a communication protocol for a remotely operated aircraft
• CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
• Flashix: modular verification of a concurrent and crash-safe flash file system
• Title not available (Why is that?)
• Program equivalence in linear contexts
• Automatic Synthesis of Assumptions for Compositional Model Checking
• Trace-based derivation of a scalable lock-free stack algorithm
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Title not available (Why is that?)
• Title not available (Why is that?)
• Compositionality Entails Sequentializability
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
• A Bibliography of Willem-Paul de Roever
• Tournaments for mutual exclusion: verification and concurrent complexity
• Compositional reasoning for shared-variable concurrent programs
• On Rely-Guarantee Reasoning
• Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models
• 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)