Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking
No abstract available.
Related papers
- Verifying Visibility-Based Weak Consistency ESOP 2020
- CDSchecker: checking concurrent data structures written with C/C++ atomics OOPSLA 2013
- RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency POPL 2025
- Verification of MPI Java programs using software model checking PPoPP 2016
- Engineering Verified Model Transformations through a Proof-Based Language Workbench SLE 2026
- Verifying correct usage of atomic blocks and typestate OOPSLA 2008
- Violat: Generating Tests of Observational Refinement for Concurrent Objects CAV 2019
- A Proof Recipe for Linearizability in Relaxed Memory Separation Logic PLDI 2024