7 citations · 15 across the 8 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
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…
cs.PL2018
Verifying C11 Programs Operationally
Simon Doherty, Brijesh Dongol, Heike Wehrheim +1
This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that the semantics is both sound and complete wit…