A. Parosh, M. F. Abdulla, B. Atig, C. Jonsson, and . Leonardsson, Stateless model checking for POWER, CAV, pp.134-156, 2016.

A. Parosh, M. F. Abdulla, T. Atig, and . Ngo, The best of both worlds: Trading efficiency and optimality in fence insertion for TSO, ESOP, pp.308-332, 2015.

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.

S. Blackshear, N. Gorogiannis, W. Peter, I. O'hearn, and . Sergey, Racerd: Compositional static race detection, Proceedings of the ACM on Programming Languages, vol.1, issue.1, 2018.

P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp.238-252, 1977.

D. Gopan and F. Dimaio, Numeric domains with summarized dimensions, TACAS, pp.512-529, 2004.

A. Gotsman, J. Berdine, B. Cook, and M. Sagiv, Thread-modular shape analysis, In ACM SIGPLAN Notices, vol.42, pp.266-277, 2007.

L. Holík, R. Meyer, T. Vojnar, and S. Wolff, Effect summaries for thread-modular analysis, SAS, pp.169-191, 2017.

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

M. Kusano and C. Wang, Flow-sensitive composition of thread-modular abstract interpretation, Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp.799-809, 2016.

M. Kusano and C. Wang, Thread-modular static analysis for relaxed memory models, Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, pp.337-348, 2017.

L. Lamport, How to make a multiprocessor computer that correctly executes multiprocess programs. Computers, IEEE Transactions on, vol.100, issue.9, pp.690-691, 1979.

J. Midtgaard, F. Nielson, and H. Nielson, Iterated process analysis over lattice-valued regular expressions, PPDP, pp.132-145, 2016.

A. Miné, Static analysis of run-time errors in embedded critical parallel C programs, ESOP, vol.11, pp.398-418, 2011.

A. Miné, Relational thread-modular static value analysis by abstract interpretation, VMCAI, pp.39-58, 2014.

R. Monat and A. Miné, Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions, VMCAI, pp.386-404, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01490178

S. Mukherjee, O. Padon, S. Shoham, D. Deepak, N. Souza et al., Thread-local semantics and its efficient sequential abstractions for racefree programs, SAS, pp.253-276, 2017.

T. Ridge, A rely-guarantee proof system for x86-TSO, International Conference on Verified Software: Theories, Tools, and Experiments, pp.55-70, 2010.

P. Sewell, S. Sarkar, and S. Owens, Francesco Zappa Nardelli, and Magnus O Myreen. x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010.

T. Suzanne and A. Miné, From array domains to abstract interpretation under store-buffer-based memory models, SAS, pp.469-488, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01360566