1 citations · 1 across the 2 of their papers we have counts for
4 papers
Implementing and Verifying Release-Acquire Transactional Memory (Extended Version)
Sadegh Dalvandi, Brijesh Dongol
Transactional memory (TM) is an intensively studied synchronisation paradigm with many proposed implementations in software and hardware, and combinations thereof. However, TM unde…
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…
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…
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…