Local rely-guarantee reasoning
From MaRDI portal
Publication:5261529
DOI10.1145/1480881.1480922zbMath1315.68088OpenAlexW2075373350MaRDI QIDQ5261529
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
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Verifying Concurrent Graph Algorithms, A perspective on specifying and verifying concurrent modules, Balancing expressiveness in formal approaches to concurrency, Proof tactics for assertions in separation logic, Steps in modular specifications for concurrent modules (invited tutorial paper), Iris from the ground up: A modular foundation for higher-order concurrent separation logic, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, Compositionality Entails Sequentializability, CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs, All-Path Reachability Logic, Program equivalence in linear contexts
