Automating Deductive Verification for Weak-Memory Programs

Alexander J. Summers, Peter Müller

Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logic…