A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
G. Schellhorn, J. Derrick, H. Wehrheim, ACM Trans. Comput. Log. (2014) 31:1--31:37.