]. P. Références1, N. B. Abdulla, G. Henda, A. Delzanno, and . Rezine, Handling parameterized systems with non-atomic global conditions, Verification, Model Checking, and Abstract Interpretation, pp.22-36, 2008.

S. V. Adve and H. Boehm, Memory models, Communications of the ACM, vol.53, issue.8, pp.90-101, 2010.
DOI : 10.1145/1787234.1787255

F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, and G. P. Rossi, Universal guards, relativization of quantifiers, and failure models in model checking modulo theories, JSAT, vol.8, issue.12, pp.29-61, 2012.

J. Alglave and L. Maranget, Stability in Weak Memory Models, CAV, pp.50-66, 2011.
DOI : 10.1007/978-3-540-30482-1_11
URL : https://hal.archives-ouvertes.fr/hal-01100806

E. A. Ashcroft, Proving assertions about parallel programs, Journal of Computer and System Sciences, vol.10, issue.1, pp.110-135, 1975.
DOI : 10.1016/S0022-0000(75)80018-3
URL : http://doi.org/10.1016/s0022-0000(75)80018-3

E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, 1982.

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, Theorem Proving in Higher Order Logics, pp.23-42, 2009.
DOI : 10.1007/978-3-540-74591-4_15

S. Conchon, A. Goel, S. Krsti´ckrsti´c, A. Mebsout, and F. Za¨?diza¨?di, Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems, CAV, pp.718-724, 2012.
DOI : 10.1007/978-3-642-31424-7_55
URL : https://hal.archives-ouvertes.fr/hal-00799272

S. Conchon, A. Goel, S. Krstic, A. Mebsout, and F. Zaidi, Invariants for finite instances and beyond, 2013 Formal Methods in Computer-Aided Design, 2013.
DOI : 10.1109/FMCAD.2013.6679392
URL : https://hal.archives-ouvertes.fr/hal-00924640

S. Conchon, A. Mebsout, and F. Za¨?diza¨?di, Vérification de systèmes paramétrés avec Cubicle, Vingtquatrì emes Journées Francophones des Langages Applicatifs, 2013.

A. Farzan and Z. Kincaid, Verification of parameterized concurrent programs by modular reasoning about data and control, POPL, pp.297-308

S. Ghilardi and S. Ranise, Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis, Logical Methods in Computer Science, vol.6, issue.4, 2010.
DOI : 10.2168/LMCS-6(4:10)2010

P. Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.174-186, 1997.
DOI : 10.1145/263699.263717

D. Hensgen, R. Finkel, and U. Manber, Two algorithms for barrier synchronization, International Journal of Parallel Programming, vol.II, issue.2, pp.1-17, 1988.
DOI : 10.1007/BF01379320

M. Herlihy and N. Shavit, The Art of Multiprocessor Programming, Revised Reprint, 2012.

K. Jiang and B. Jonsson, Using spin to model check concurrent algorithms, using a translation from c to promela, Second Swedish Workshop on Multi-Core Computing, 2009.

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.207-220, 2009.
DOI : 10.1145/1629575.1629596

]. L. Lamport, How to make a correct multiprocess program execute correctly on a multiprocessor, IEEE Transactions on Computers, vol.46, issue.7, 1979.
DOI : 10.1109/12.599898

D. Le, W. Chin, and Y. Teo, Verfication of static and dynamic barrier synchronization using bounded permissions, ICFEM, 2013.

J. Lee and D. Padua, Hiding relaxed memory consistency with a compiler, IEEE Transactions on Computers, vol.50, issue.8, pp.824-833, 2001.
DOI : 10.1109/12.947002

N. A. Lynch, Distributed algorithms, 1996.

M. Musuvathi, D. Y. Park, A. Chou, D. R. Engler, and D. L. Dill, CMC, ACM SIGOPS Operating Systems Review, vol.36, issue.SI, pp.75-88, 2002.
DOI : 10.1145/844128.844136

M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar et al., Finding and reproducing heisenbugs in concurrent programs, Proceedings of the 8th USENIX conference on Operating systems design and implementation, pp.267-280, 2008.

S. Owicki and D. Gries, An axiomatic proof technique for parallel programs I, Acta Informatica, vol.11, issue.4, pp.319-340, 1976.
DOI : 10.1007/BF00268134

A. Pnueli, S. Ruah, and L. Zuck, Automatic Deductive Verification with Invisible Invariants, TACAS, pp.82-97, 2001.
DOI : 10.1007/3-540-45319-9_7

J. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR, International Symposium on Programming, pp.337-351, 1982.
DOI : 10.1007/3-540-11494-7_22