R. Bedin-frança, S. Blazy, D. Favre-felix, X. Leroy, M. Pantel et al., Formally verified optimizing compilation in ACG-based flight control software, 2012.

F. Besson, S. Blazy, and P. Wilke, A Precise and Abstract Memory Model for C Using Symbolic Values, APLAS, 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/s10817-009-9148-3

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

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

E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, and M. Moskal, VCC: A Practical System for Verifying Concurrent C, TPHOLs, 2009.
DOI : 10.1007/978-3-540-74591-4_15

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

C. Ellison and G. Ro¸suro¸su, An executable formal semantics of C with applications, POPL. ACM, 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, PLDI. ACM, 2014.

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

J. Kang, C. Hur, W. Mansky, D. Garbuzov, S. Zdancewic et al., A formal C memory model supporting integer-pointer casts, PLDI. ACM, 2015.

R. Krebbers, Aliasing Restrictions of C11 Formalized in Coq, CPP, 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

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, 2009.
DOI : 10.1145/1538788.1538814

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

X. Leroy, A. W. Appel, S. Blazy, and G. Stewart, The CompCert memory model, Program Logics for Certified Compilers, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00905435

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/s10817-008-9099-0

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

M. Norrish, C formalised in HOL, 1998.

H. Tuch, G. Klein, and M. Norrish, Types, bytes, and separation logic, POPL. ACM, 2007.

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

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, PLDI. ACM, 2011.