Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study
Abstract elided by the publisher.
Related papers
- CheckFence: checking consistency of concurrent data types on relaxed memory models PLDI 2007
- Model checking copy phases of concurrent copying garbage collection with various memory models OOPSLA 2017
- Dynamic partial order reduction for relaxed memory models PLDI 2015
- RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency POPL 2025
- Compiler Testing with Relaxed Memory Models CGO 2024
- Bounded Model Checking for Asynchronous Hyperproperties TACAS 2023
- Verifying observational robustness against a c11-style memory model POPL 2021
- Bounded Model Checking for Hyperproperties TACAS 2021