Verifying read-copy-update in a logic for weak memory.

Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis

Browse the full PLDI paper archive.