Parameterized Memory Models and Concurrent Separation Logic
Abstract elided by the publisher.
Related papers
- Relaxed separation logic: a program logic for C11 concurrency OOPSLA 2013
- Cosmo: a concurrent separation logic for multicore OCaml ICFP 2020
- Iron: managing obligations in higher-order concurrent separation logic POPL 2019
- SecRSL: security separation logic for C11 release-acquire concurrency OOPSLA 2021
- Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA 2023
- A Separation Logic for a Promising Semantics ESOP 2018
- Formal verification of a concurrent bounded queue in a weak memory model ICFP 2021
- Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic PLDI 2025