Verifying C11-Style Weak Memory Libraries via Refinement

Sadegh Dalvandi, Brijesh Dongol

Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalability, we also require modular…