M. P. 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

S. Gilbert and N. Lynch, Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services, ACM SIGACT News, vol.33, issue.2, pp.51-59, 2002.
DOI : 10.1145/564585.564601

P. B. Gibbons and E. Korach, Testing Shared Memories, SIAM Journal on Computing, vol.26, issue.4, pp.1208-1244, 1997.
DOI : 10.1137/S0097539794279614
URL : http://www.pittsburgh.intel-research.net/people/gibbons/papers/tsm.pdf

J. M. Wing and C. Gong, Testing and Verifying Concurrent Objects, Journal of Parallel and Distributed Computing, vol.17, issue.1-2, pp.164-182, 1993.
DOI : 10.1006/jpdc.1993.1015

G. Lowe, Testing for linearizability, Concurrency and Computation: Practice and Experience, vol.21, issue.7
DOI : 10.1145/359545.359563

A. Bouajjani, M. Emmi, C. Enea, and J. Hamza, Tractable refinement checking for concurrent objects, pp.651-662, 2015.
DOI : 10.1145/2775051.2677002

I. Rabinovitch, The dimension of semiorders, Journal of Combinatorial Theory, Series A, vol.25, issue.1, pp.50-61, 1978.
DOI : 10.1016/0097-3165(78)90030-4

C. Okasaki, Purely Functional Data Structures, 1998.
DOI : 10.1017/CBO9780511530104

K. Kingsbury, Computational techniques in Knossos. https://aphyr.com/posts/ 314-computational-techniques-in-knossos, 2014.

A. Aiyer, L. Alvisi, and R. A. Bazzi, On the Availability of Non-strict Quorum Systems, Proceedings of the 19th International Conference on Distributed Computing. DISC'05, pp.48-62, 2005.
DOI : 10.1007/11561927_6

L. Wang and S. D. Stoller, Static analysis of atomicity for programs with non-blocking synchronization, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming , PPoPP '05, pp.61-71, 2005.
DOI : 10.1145/1065944.1065953

A. Bouajjani, M. Emmi, C. Enea, and J. Hamza, Verifying Concurrent Programs against Sequential Specifications, pp.290-309, 2013.
DOI : 10.1007/978-3-642-37036-6_17
URL : http://www.liafa.univ-paris-diderot.fr/~cenea/esop2013-lin-long.pdf

R. Alur, K. Mcmillan, and D. Peled, Model-Checking of Correctness Conditions for Concurrent Objects, Information and Computation, vol.160, issue.1-2, pp.167-188, 2000.
DOI : 10.1006/inco.1999.2847

R. Colvin, S. Doherty, and L. Groves, Verifying Concurrent Data Structures by Simulation, Electronic Notes in Theoretical Computer Science, vol.137, issue.2, pp.93-110, 2005.
DOI : 10.1016/j.entcs.2005.04.026

J. Derrick, G. Schellhorn, and H. Wehrheim, Mechanically verified proof obligations for linearizability, ACM Transactions on Programming Languages and Systems, vol.33, issue.1, pp.1-443, 2011.
DOI : 10.1145/1889997.1890001

M. Vechev, E. Yahav, and G. Yorsh, Experience with Model Checking Linearizability, pp.261-278, 2009.
DOI : 10.1006/jpdc.1993.1015

S. Burckhardt, C. Dern, M. Musuvathi, and R. Tan, Line-up, ACM SIGPLAN Notices, vol.45, issue.6, pp.330-340, 2010.
DOI : 10.1145/1809028.1806634

?. Cern´ycern´-cern´y, P. Radhakrishna, A. Zufferey, D. Chaudhuri, S. Alur et al., Model checking of linearizability of concurrent list implementations, pp.10-465, 2010.

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

D. Amit, N. Rinetzky, T. Reps, M. Sagiv, and E. Yahav, Comparison Under Abstraction for Verifying Linearizability, CAV'07, pp.477-490, 2007.
DOI : 10.1007/978-3-540-73368-3_49
URL : http://www.cs.tau.ac.il/~msagiv/cav07d.pdf

J. Berdine, T. Lev-ami, R. Manevich, G. Ramalingam, and M. Sagiv, Thread Quantification for Concurrent Shape Analysis, CAV '08, pp.399-413, 2008.
DOI : 10.1007/978-3-540-70545-1_37
URL : http://www.cs.tau.ac.il/~rumster/tq.pdf

V. Vafeiadis, Shape-Value Abstraction for Verifying Linearizability, VMCAI '09, pp.335-348, 2009.
DOI : 10.1016/S1571-0661(05)80006-4

V. Vafeiadis, Automatically Proving Linearizability, pp.450-464, 2010.
DOI : 10.1007/978-3-642-14295-6_40
URL : http://www.cl.cam.ac.uk/%7Evv216/papers/cav2010-linear.pdf

E. Anderson, X. Li, M. A. Shah, J. Tucek, and J. J. Wylie, What consistency does your key-value store actually provide? HotDep'10, pp.1-16, 2010.

O. Shacham, N. Bronson, A. Aiken, M. Sagiv, M. Vechev et al., Testing atomicity of composed concurrent operations, ACM SIGPLAN Notices, vol.46, issue.10, pp.51-64, 2011.
DOI : 10.1145/2076021.2048073

P. Fonseca, C. Li, and R. Rodrigues, Finding complex concurrency bugs in large multithreaded applications, pp.215-228, 2011.
DOI : 10.1145/1966445.1966465
URL : http://www.mpi-sws.org/~rodrigo/eurosys11-pike.pdf

M. Pradel and T. R. Gross, Fully automatic and precise detection of thread safety violations, ACM SIGPLAN Notices, vol.47, issue.6, pp.521-530, 2012.
DOI : 10.1145/1950365.1950395

M. Pradel and T. R. Gross, Automatic testing of sequential and concurrent substitutability, 2013 35th International Conference on Software Engineering (ICSE), pp.282-291, 2013.
DOI : 10.1109/ICSE.2013.6606574

W. Golab, J. Hurwitz, and X. S. Li, On the k-Atomicity-Verification Problem, 2013 IEEE 33rd International Conference on Distributed Computing Systems, pp.591-600, 2013.
DOI : 10.1109/ICDCS.2013.45
URL : http://static.googleusercontent.com/external_content/untrusted_dlcp/research.google.com/en/us/pubs/archive/41097.pdf

T. Elmas, S. Tasiran, and S. Qadeer, VYRD, ACM SIGPLAN Notices, vol.40, issue.6, pp.27-37, 2005.
DOI : 10.1145/1064978.1065015