A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. - SCHELLHORN, GERHARD; DERRICK, JOHN; WEHRHEIM, HEIKE (ACM Transactions on Computational Logic, 2014)