Modular Reasoning about Separation of Concurrent Data Structures
No abstract available.
Related papers
- Modular Verification of State-Based CRDTs in Separation Logic ECOOP 2023
- Local Reasoning for Global Graph Properties ESOP 2020
- Modular verification of heap reachability properties in separation logic OOPSLA 2019
- Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA 2023
- Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs ICFP 2025
- Formal verification of a concurrent bounded queue in a weak memory model ICFP 2021
- Verifying concurrent search structure templates PLDI 2020
- Verifying Lock-Free Search Structure Templates ECOOP 2024