A Separation Logic for Fictional Sequential Consistency
Abstract elided by the publisher.
Related papers
- Fictional Separation Logic ESOP 2012
- Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic PLDI 2025
- Separation logic for sequential programs (functional pearl) ICFP 2020
- Concurrent Abstract Predicates ECOOP 2010
- Program Verification Under Weak Memory Consistency Using Separation Logic CAV 2017
- Cosmo: a concurrent separation logic for multicore OCaml ICFP 2020
- Proof-Directed Parallelization Synthesis by Separation Logic TOPLAS 2013
- Towards certified separate compilation for concurrent programs PLDI 2019