Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning
S. Tasiran, A. Sezgin, and S. Quadeer. Design and Validation of Concurrent Systems, 09361, Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, (2010)