Showing cs.PLShow all
2 papers · 1 filter
cs.PL2020
Verifying C11-Style Weak Memory Libraries
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 scalabiility, we also require modula…
cs.PL2020
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
Sadegh Dalvandi, Brijesh Dongol, Simon Doherty
Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work…