B. França, R. Blazy, S. Favre-felix, D. Leroy, X. Pantel et al., Formally verified optimizing compilation in ACG-based flight control software, p.2, 2012.

D. J. Bernstein, T. Lange, and P. Schwabe, The Security Impact of a New Cryptographic Library, LATINCRYPT'12, pp.159-176, 2012.
DOI : 10.1007/978-3-642-33481-8_9

F. Besson, S. Blazy, and P. Wilke, Companion website with Coq development

F. Besson, S. Blazy, and P. Wilke, A Precise and Abstract Memory Model for C Using Symbolic Values, APLAS, LNCS, 2014.
DOI : 10.1007/978-3-319-12736-1_24
URL : https://hal.archives-ouvertes.fr/hal-01093312

S. Blazy, Experiments in validating formal semantics for C, Raboud University Nijmegen report ICIS-R07015, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00292043

S. Blazy and X. Leroy, Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning, vol.29, issue.6, 2009.
DOI : 10.1007/3-540-56992-8_17
URL : https://hal.archives-ouvertes.fr/inria-00352524

Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao, End-to-end verification of stack-space bounds for C programs, PLDI '14, p.30, 2014.

A. T. Clements, M. F. Kaashoek, N. Zeldovich, R. T. Morris, and E. Kohler, The scalable commutativity rule: designing scalable software for multicore processors, 2013.

E. Cohen, M. Moskal, S. Tobies, and W. Schulte, A Precise Yet Efficient Memory Model For C, Electronic Notes in Theoretical Computer Science, vol.254, 2009.
DOI : 10.1016/j.entcs.2009.09.061
URL : https://doi.org/10.1016/j.entcs.2009.09.061

C. Ellison and G. Ro¸suro¸su, An executable formal semantics of C with applications, 2012.

D. Greenaway, J. Andronick, and G. Klein, Bridging the Gap: Automatic Verified Abstraction of C, ITP, 2012.
DOI : 10.1007/978-3-642-32347-8_8

D. Greenaway, J. Lim, J. Andronick, and G. Klein, Don't sweat the small stuff: formal verification of C code without the pain, 2014.

C. Hathhorn, C. Ellison, and G. Ro¸suro¸su, Defining the undefinedness of c, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), pp.336-345, 2015.

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-verified C static analyzer, In: POPL, 2015.
DOI : 10.1145/2775051.2676966
URL : https://hal.archives-ouvertes.fr/hal-01078386

J. Kang, C. K. Hur, W. Mansky, D. Garbuzov, S. Zdancewic et al., A formal C memory model supporting integer-pointer casts, 2015.
DOI : 10.1145/2737924.2738005
URL : http://sf.snu.ac.kr/gil.hur/publications/intptrcast.pdf

R. Krebbers, Aliasing Restrictions of C11 Formalized in Coq, CPP, LNCS, pp.978-981, 2013.
DOI : 10.1007/978-3-319-03545-1_4

R. Krebbers, An operational and axiomatic semantics for non-determinism and sequence points in C, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, 2014.
DOI : 10.1145/2535838.2535878

R. Krebbers, X. Leroy, and F. Wiedijk, Formal C Semantics: CompCert and the C Standard, ITP 2014, 2014.
DOI : 10.1007/978-3-319-08970-6_36
URL : https://hal.archives-ouvertes.fr/hal-00981212

D. Lee, A memory allocator Leroy, X.: Formal verification of a realistic compiler, C. ACM, vol.52, issue.7, 2009.

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/978-3-642-59495-3
URL : https://hal.archives-ouvertes.fr/inria-00360768

X. Leroy, A. W. Appel, S. Blazy, and G. Stewart, The CompCert memory model In: Program Logics for Certified Compilers, 2014.

X. Leroy and S. Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, vol.17, issue.5???6, 2008.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/inria-00289542

M. Ltd, :. M. Misra-c-l, and N. Bjørner, Guidelines for the use of the C language in critical systems, Z3: An Efficient SMT Solver. In: TACAS, LNCS, 2004.

M. Norrish, C formalised in HOL, 1998.

H. Tuch, G. Klein, and M. Norrish, Types, bytes, and separation logic, 2007.
DOI : 10.1145/1190216.1190234
URL : http://www.nicta.com.au/people/norrishm/attachments/bibliographies_and_papers/2007/popl2007.pdf

X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich et al., Undefined behavior, Proceedings of the Asia-Pacific Workshop on Systems, APSYS '12, p.12, 2012.
DOI : 10.1145/2349896.2349905

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, 2011.
DOI : 10.1145/1993316.1993532