Proving correctness of highly-concurrent linearisable objects.

Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro

Browse the full PPoPP paper archive.