S. V. Adve and J. K. Aggarwal, A unified formalization of four shared-memory models, IEEE Transactions on Parallel and Distributed Systems, vol.4, issue.6, pp.613-624, 1993.
DOI : 10.1109/71.242161

A. Armstrong, B. Dongol, and S. Doherty, Reducing Opacity to Linearizability: A Sound and Complete Method. ArXiv e-prints, 1610.

H. Attiya, A. Gotsman, S. Hans, and N. Rinetzky, A programming language perspective on transactional memory consistency, Proceedings of the 2013 ACM symposium on Principles of distributed computing, PODC '13, pp.309-318, 2013.
DOI : 10.1145/2484239.2484267

A. Bouajjani, M. Emmi, C. Enea, and J. Hamza, On Reducing Linearizability to State Reachability, LNCS, vol.9135, pp.95-107, 2015.
DOI : 10.1007/978-3-662-47666-6_8

P. Cern´ycern´y, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, Model checking of linearizability of concurrent list implementations, CAV. LNCS, pp.465-479, 2010.

S. Chakraborty, T. A. Henzinger, A. Sezgin, and V. Vafeiadis, Aspect-oriented linearizability proofs, Logical Methods in Computer Science, vol.11, issue.1, 2015.
DOI : 10.2168/LMCS-11(1:20)2015

L. Dalessandro, D. Dice, M. L. Scott, N. Shavit, and M. F. Spear, Transactional Mutex Locks, Euro-Par, pp.2-13, 2010.
DOI : 10.1109/CGO.2009.30

URL : http://www.cs.rochester.edu/u/scott/papers/2009_TRANSACT_TML.pdf

L. Dalessandro, M. F. Spear, and M. L. Scott, NORec: streamlining STM by abolishing ownership records, pp.67-78, 2010.

J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim, Verifying Opacity of a Transactional Mutex Lock, FM. LNCS, pp.161-177, 2015.
DOI : 10.1007/978-3-319-19249-9_11

S. Doherty, L. Groves, V. Luchangco, and M. Moir, Formal Verification of a??Practical Lock-Free Queue Algorithm, FORTE. LNCS, pp.97-114, 2004.
DOI : 10.1006/inco.1995.1134

S. Doherty, L. Groves, V. Luchangco, and M. Moir, Towards formally specifying and verifying transactional memory. Formal Asp, Comput, vol.25, issue.5, pp.769-799, 2013.
DOI : 10.1007/s00165-012-0225-8

URL : http://research.sun.com/people/moir/pubs/Refine09-TM-correctness.pdf

B. Dongol and J. Derrick, Verifying Linearisability, ACM Computing Surveys, vol.48, issue.2, p.19, 2015.
DOI : 10.1007/978-3-642-29952-0_12

R. Guerraoui, T. A. Henzinger, and V. Singh, Model checking transactional memories, Distributed Computing, vol.54, issue.4, pp.129-145, 2010.
DOI : 10.1007/s00446-009-0092-6

R. Guerraoui and M. Kapalka, On the correctness of transactional memory, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming , PPoPP '08, pp.175-184, 2008.
DOI : 10.1145/1345206.1345233

R. Guerraoui and M. Kapalka, Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory, 2010.

T. Harris, J. R. Larus, and R. Rajwar, Transactional Memory, Synthesis Lectures on Computer Architecture, 2010.
DOI : 10.1201/b11417-16

M. Herlihy and J. M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems, vol.12, issue.3, pp.463-492, 1990.
DOI : 10.1145/78969.78972

C. A. Hoare, Communicating sequential processes, Communications of the ACM, vol.21, issue.8, pp.666-677, 1978.
DOI : 10.1145/359576.359585

E. Koskinen and M. Parkinson, The push/pull model of transactions, PLDI. PLDI '15, pp.186-195, 2015.

M. Lesani, V. Luchangco, and M. Moir, A Framework for Formally Verifying Software Transactional Memory Algorithms, pp.516-530, 2012.
DOI : 10.1007/978-3-642-32940-1_36

M. Lesani, V. Luchangco, and M. Moir, Putting opacity in its place, 2012.

M. Lesani and J. Palsberg, Decomposing Opacity, LNCS, vol.8784, pp.391-405, 2014.
DOI : 10.1007/978-3-662-45174-8_27

Y. Liu, W. Chen, Y. A. Liu, J. Sun, S. J. Zhang et al., Verifying Linearizability via Optimized Refinement Checking, IEEE Transactions on Software Engineering, vol.39, issue.7, pp.1018-1039, 2013.
DOI : 10.1109/TSE.2012.82

URL : http://research.microsoft.com/en-us/people/weic/tse13_linearizability.pdf

S. Owens, Reasoning about the Implementation of Concurrency Abstractions on x86-TSO, ECOOP 2010, pp.478-503, 2010.
DOI : 10.1007/978-3-642-14107-2_23

G. Schellhorn, J. Derrick, and H. Wehrheim, A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures, ACM Transactions on Computational Logic, vol.15, issue.4, pp.1-3137, 2014.
DOI : 10.1145/1122971.1122992

J. Sun, Y. Liu, J. S. Dong, and J. Pang, PAT: Towards Flexible Verification under Fairness, CAV. LNCS, pp.709-714, 2009.
DOI : 10.1007/3-540-10843-2_22

URL : http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf

V. Vafeiadis, Modular fine-grained concurrency verification, 2007.