R. Bedin-franca, S. Blazy, D. Favre-felix, X. Leroy, M. Pantel et al., Formally verified optimizing compilation in ACG-based flight control software, ERTS 2012: Embedded Real Time Software and Systems, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00653367

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

F. Besson, S. Blazy, and P. Wilke, A Concrete Memory Model for CompCert, ITP, 2015.
DOI : 10.1007/978-3-319-22102-1_5
URL : https://hal.archives-ouvertes.fr/hal-01194549

S. Blazy and A. Trieu, Formal verification of control-flow graph flattening, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, 2016.
DOI : 10.1109/MC.1984.1659158
URL : https://hal.archives-ouvertes.fr/hal-01242063

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

C. Hathhorn, C. Ellison, and G. Rosu, Defining the undefinedness of C, PLDI. ACM, 2015.

J. Kang, C. Hur, W. Mansky, D. Garbuzov, S. Zdancewic et al., A formal C memory model supporting integer-pointer casts, PLDI, 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, 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

J. A. Kroll, G. Stewart, and A. W. Appel, Portable Software Fault Isolation, 2014 IEEE 27th Computer Security Foundations Symposium, 2014.
DOI : 10.1109/CSF.2014.10
URL : http://doi.org/10.1109/csf.2014.10

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

K. Memarian, J. Matthiesen, J. Lingard, K. Nienhuis, D. Chisnall et al., Into the depths of C: elaborating the de facto standards, PLDI, 2016.

M. Norrish, C formalised in HOL, 1998.

V. Robert and X. Leroy, A Formally-Verified Alias Analysis, CPP, 2012.
DOI : 10.1007/978-3-642-35308-6_5
URL : https://hal.archives-ouvertes.fr/hal-00773109