Weak updates and separation logic
Abstract elided by the publisher.
Related papers
- Program Verification Under Weak Memory Consistency Using Separation Logic CAV 2017
- Verifying read-copy-update in a logic for weak memory PLDI 2015
- Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA 2023
- Reasoning about Weak Isolation Levels in Separation Logic ICFP 2025
- The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic CPP 2025
- SecRSL: security separation logic for C11 release-acquire concurrency OOPSLA 2021
- Context logic and tree update POPL 2005
- Fluid Updates: Beyond Strong vs. Weak Updates ESOP 2010