Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)

Ömer Şakar, Soham Chakraborty, Marieke Huisman +1

Concurrent programming under weak memory concurrency faces substantial challenges to ensure correctness due to program behaviors that cannot be explained by thread interleaving, a.…