Mechanically verified proof obligations for linearizability
J. Derrick, G. Schellhorn, H. Wehrheim, ACM Trans. Program. Lang. Syst. (2011) 4:1--4:43.