V. Sarita, K. Adve, and . Gharachorloo, Shared memory consistency models: A tutorial, computer, vol.29, issue.12, pp.66-76, 1996.

J. Alglave, D. Kroening, J. Lugton, V. Nimal, and M. Tautschnig, Soundness of Data Flow Analyses for Weak Memory Models, Programming Languages and Systems, pp.272-288, 2011.
DOI : 10.1145/186025.186043

J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig, Software Verification for Weak Memory via Program Transformation, Programming Languages and Systems, pp.512-532, 2013.
DOI : 10.1007/978-3-642-37036-6_28

M. Faouzi-atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi, On the verification problem for weak memory models, ACM SIGPLAN Notices, vol.45, issue.1, pp.7-18, 2010.
DOI : 10.1145/1707801.1706303

A. Bouajjani, E. Derevenetc, and R. Meyer, Checking and Enforcing Robustness against TSO, Programming Languages and Systems, pp.533-553, 2013.
DOI : 10.1007/978-3-642-37036-6_29

F. Bourdoncle, Efficient chaotic iteration strategies with widenings, Formal Methods in Programming and their Applications, pp.128-141, 1993.
DOI : 10.1007/BFb0039704

J. Sylvain-conchon, J. Filliâtre, and . Signoles, Designing a generic graph library using ml functors. Trends in functional programming, pp.124-140, 2007.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/hal-01108790

P. Cousot, R. Cousot, and F. Logozzo, A parametric segmentation functor for fully automatic and scalable array content analysis, ACM SIGPLAN Notices, vol.46, issue.1, pp.105-118, 2011.
DOI : 10.1145/1925844.1926399

URL : https://hal.archives-ouvertes.fr/inria-00543874

A. Dan, Y. Meshman, M. Vechev, and E. Yahav, Effective abstractions for verification under relaxed memory models, Verification, Model Checking , and Abstract Interpretation, pp.449-466, 2014.

D. Gopan and F. Dimaio, Nurit Dor, Thomas Reps, and Mooly Sagiv Numeric domains with summarized dimensions, Tools and Algorithms for the Construction and Analysis of Systems, pp.512-529, 2004.

B. Jeannet, The bddapron logico-numerical abstract domains library, 2009.

B. Jeannet and A. Miné, Apron: A Library of Numerical Abstract Domains for Static Analysis, Computer Aided Verification, pp.661-667, 2009.
DOI : 10.1007/978-3-642-02658-4_52

URL : https://hal.archives-ouvertes.fr/hal-00786354

M. Kuperstein, M. Vechev, and E. Yahav, Partial-coherence abstractions for relaxed memory models, ACM SIGPLAN Notices, vol.46, issue.6, pp.187-198, 2011.
DOI : 10.1145/1993316.1993521

M. Kuperstein, M. Vechev, and E. Yahav, Automatic inference of memory fences, ACM SIGACT News, vol.43, issue.2, pp.108-123, 2012.
DOI : 10.1145/2261417.2261438

L. Lamport, How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, IEEE Transactions on Computers, vol.28, issue.9, pp.690-691, 1979.
DOI : 10.1109/TC.1979.1675439

Y. Meshman, A. Dan, M. Vechev, and E. Yahav, Synthesis of Memory Fences via Refinement Propagation, Static Analysis, pp.237-252, 2014.
DOI : 10.1007/978-3-319-10936-7_15

L. Gary and . Peterson, Myths about the mutual exclusion problem, Information Processing Letters, vol.12, issue.3, pp.115-116, 1981.

P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen, x86-TSO, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010.
DOI : 10.1145/1785414.1785443

H. Siegel and A. Simon, Summarized Dimensions Revisited, Electronic Notes in Theoretical Computer Science, vol.288, pp.75-86, 2012.
DOI : 10.1016/j.entcs.2012.10.009