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, LNCS, vol.8858, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01093312

F. Besson, S. Blazy, and P. Wilke, A concrete memory model for CompCert, ITP, LNCS, vol.9236, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01194549

F. Besson, S. Blazy, and P. Wilke, A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data, Journal of Automated Reasoning, pp.1-48, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01656895

S. Blazy and A. Trieu, Formal verification of control-flow graph flattening, CPP. ACM, 2016.
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, 2014.

C. Ellison and G. Rosu, An executable formal semantics of C with applications, SIGPLAN Not, vol.47, issue.1, 2012.

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

. Iso:-iso-c-standard, , 1999.

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

R. Krebbers, Aliasing restrictions of C11 formalized in Coq, CPP, LNCS, vol.8307, 2013.

R. Krebbers, An operational and axiomatic semantics for non-determinism and sequence points in C, 2014.

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

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.41, issue.1, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00289542

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

E. Mullen, D. Zuniga, Z. Tatlock, and D. Grossman, Verified peephole optimizations for CompCert, pp.448-461, 2016.

M. Norrish, C formalised in hol, 1998.

V. Robert and X. Leroy, A formally-verified alias analysis, CPP, LNCS, vol.7679, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00773109

J. ?ev?ík, V. Vafeiadis, F. Zappa-nardelli, S. Jagannathan, and P. Sewell, CompCertTSO: A verified compiler for relaxed-memory concurrency, J. ACM, vol.60, issue.3, p.50, 2013.