M. Abadi and L. Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems, vol.17, issue.3, pp.507-534, 1995.
DOI : 10.1145/203095.201069

R. Bayer and M. Schkolnick, Concurrency of operations on B-trees, Acta Informatica, vol.9, issue.1, pp.1-21, 1977.
DOI : 10.1007/BF00263762

S. Doherty, L. Groves, V. Luchangco, and M. Moir, Formal Verification of a??Practical Lock-Free Queue Algorithm, Int. Conf. on Formal Techniques for Networked and Dist. Sys, pp.97-114, 2004.
DOI : 10.1007/978-3-540-30232-2_7

C. Flanagan, S. N. Freund, S. Qadeer, and S. A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, vol.338, issue.1-3, pp.1-3153, 2005.
DOI : 10.1016/j.tcs.2004.12.006

H. Gao, J. F. Groote, and W. H. Hesselink, Lock-free dynamic hash tables with open addressing, Distributed Computing, vol.JD, issue.1, pp.21-42, 2005.
DOI : 10.1007/s00446-004-0115-2

J. V. Guttag, E. Horowitz, and D. R. Musser, Abstract data types and software validation, Communications of the ACM, vol.21, issue.12, pp.1048-1064, 1978.
DOI : 10.1145/359657.359666

T. Harris, A Pragmatic Implementation of Non-blocking Linked-lists, Lecture Notes in Computer Science, vol.2180, pp.300-314, 2001.
DOI : 10.1007/3-540-45414-4_21

S. Heller, M. Herlihy, V. Luchangco, M. Moir, B. Scherer et al., A lazy concurrent list-based set algorithm, 9th International Conference on Principles of Distributed Systems (OPODIS), 2005.

T. A. Henzinger, S. Qadeer, and S. K. Rajamani, You assume, we guarantee: Methodology and case studies, Int. Conf. on Computer-Aided Verification (CAV), pp.440-451, 1998.
DOI : 10.1007/BFb0028765

M. Herlihy and J. 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

B. Jacobs, K. R. Leino, and W. Schulte, Verification of multithreaded object-oriented programs with invariants, W. on Specification and Verification of Component-Based Systems, 2004.

C. B. Jones, Specification and design of (parallel) programs, IFIP Congress, pp.321-332, 1983.

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

L. Lamport, Composition: A Way to Make Proofs Harder, Proc. COMPOS'97 Symp., volume 1536 of Lecture Notes in Computer Science, pp.402-423, 1997.
DOI : 10.1007/3-540-49213-5_15

D. Lea, Concurrent hash map in JSR166 concurrency utilities

N. A. Lynch and M. R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing , PODC '87, pp.137-151, 1987.
DOI : 10.1145/41840.41852

M. Michael, High performance dynamic lock-free hash tables and list-based sets, Proceedings of the fourteenth annual ACM symposium on Parallel algorithms and architectures , SPAA '02, pp.73-82, 2002.
DOI : 10.1145/564870.564881

M. Michael and M. Scott, Nonblocking Algorithms and Preemption-Safe Locking on Multiprogrammed Shared Memory Multiprocessors, Journal of Parallel and Distributed Computing, vol.51, issue.1, pp.1-26, 1998.
DOI : 10.1006/jpdc.1998.1446

P. W. O-'hearn, Resources, concurrency and local reasoning, In CONCUR, pp.49-67, 2004.

S. Owicki and D. Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, vol.19, issue.5, pp.279-285, 1976.
DOI : 10.1145/360051.360224

V. Vafeiadis, M. Herlihy, T. Hoare, and M. Shapiro, A safety proof of a lazy concurrent list-based set implementation, 2006.