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, ERTS2 2012: Embedded Real Time Software and Systems, 2012.

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

S. Blazy and X. Leroy, Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning, vol.29, issue.6, pp.263-288, 2009.
DOI : 10.1007/s10817-009-9148-3
URL : https://hal.archives-ouvertes.fr/inria-00352524

E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, TPHOLs, pp.23-42, 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, pp.85-103, 2009.
DOI : 10.1016/j.entcs.2009.09.061

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

C. Ellison and G. Ro¸suro¸su, An executable formal semantics of C with applications, POPL, pp.533-544, 2012.

D. Greenaway, J. Andronick, and G. Klein, Bridging the Gap: Automatic Verified Abstraction of C, ITP, pp.99-115, 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.

R. Krebbers, Aliasing Restrictions of C11 Formalized in Coq, CPP, pp.50-65, 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, pp.101-112, 2014.
DOI : 10.1145/2535838.2535878

D. Lee, A memory allocator

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

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

D. Lucanu, T. F. , and G. Ro¸suro¸su, K Framework Distilled, Workshop on Rewriting Logic and its Applications, pp.31-53, 2012.

M. Norrish, C formalised in HOL, 1998.

H. Tuch, G. Klein, and M. Norrish, Types, bytes, and separation logic, POPL, pp.97-108, 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, pp.1-7, 2012.
DOI : 10.1145/2349896.2349905

X. Wang, N. Zeldovich, M. F. Kaashoek, and A. Solar-lezama, Towards optimization-safe systems, Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP '13, pp.260-275, 2013.
DOI : 10.1145/2517349.2522728