A Marriage of Rely/Guarantee and Separation Logic

DOI10.1007/978-3-540-74407-8_18zbMath1151.68556OpenAlexW1819989006MaRDI QIDQ3525642

Viktor Vafeiadis, Matthew J. Parkinson

Publication date: 18 September 2008

Published in: CONCUR 2007 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74407-8_18

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction, Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Certifying low-level programs with hardware interrupts and preemptive threads, A temporal programming model with atomic blocks based on projection temporal logic, Automated Theorem Proving for Assertions in Separation Logic with All Connectives, Completeness for a First-Order Abstract Separation Logic, Formal verification of concurrent programs with Read-write locks, Revisiting concurrent separation logic, Inter-process buffers in separation logic with rely-guarantee, Separation logics and modalities: a survey, Balancing expressiveness in formal approaches to concurrency, Proof tactics for assertions in separation logic, Verifying a concurrent garbage collector using a rely-guarantee methodology, Effect algebras, Girard quantales and complementation in separation logic, Compositional verification of a communication protocol for a remotely operated aircraft, Iris from the ground up: A modular foundation for higher-order concurrent separation logic, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, Abstract Specifications for Concurrent Maps, Explanation of two non-blocking shared-variable communication algorithms, A dynamic logic for deductive verification of multi-threaded programs, CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs, RGITL: a temporal logic framework for compositional reasoning about interleaved programs, Weak updates and separation logic, All-Path Reachability Logic, Proving linearizability with temporal logic, Concurrent Separation Logic and Operational Semantics, Algebraic separation logic, Ott: Effective tool support for the working semanticist, Towards a Thread-Local Proof Technique for Starvation Freedom, Automatically verifying temporal properties of pointer programs with cyclic proof, Granularity and Concurrent Separation Logic, A Machine-Checked Framework for Relational Separation Logic, Fine-grained concurrency with separation logic, Verifying a concurrent garbage collector with a rely-guarantee methodology, Decision problems in a logic for reasoning about reconfigurable distributed systems, Program equivalence in linear contexts, On the relation between concurrent separation logic and concurrent Kleene algebra, Reasoning about Separation Using Abstraction and Reification