Local rely-guarantee reasoning
DOI10.1145/1480881.1480922zbMATH Open1315.68088OpenAlexW2075373350MaRDI QIDQ5261529FDOQ5261529
Publication date: 3 July 2015
Published in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1480881.1480922
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cited In (18)
- Steps in modular specifications for concurrent modules (invited tutorial paper)
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
- Program equivalence in linear contexts
- Balancing expressiveness in formal approaches to concurrency
- Using Locales to Define a Rely-Guarantee Temporal Logic
- A Marriage of Rely/Guarantee and Separation Logic
- A perspective on specifying and verifying concurrent modules
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement
- Compositionality Entails Sequentializability
- Verifying Concurrent Graph Algorithms
- Deny-Guarantee Reasoning
- Proof tactics for assertions in separation logic
- All-Path Reachability Logic
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Ownership guided C to Rust translation
- Specifying and reasoning about shared-variable concurrency
- Compositional reasoning for non-multicopy atomic architectures
This page was built for publication: Local rely-guarantee reasoning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5261529)
