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

R. Krebbers and F. Wiedijk, Separation Logic for Non-local Control Flow and Block Scope Variables, FoSSaCS. LNCS, pp.257-272, 2013.
DOI : 10.1007/978-3-642-37075-5_17

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, Version 2, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00703441

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, pp.1-31, 2008.
DOI : 10.1007/s10817-008-9099-0
URL : https://hal.archives-ouvertes.fr/inria-00289542

Y. Moy and C. Marché, The Jessie plugin for Deduction Verification in, 2011.

M. Norrish, C formalised in HOL, 1998.

J. Regehr, Blog post at http://blog.regehr.org/archives, p.759, 2012.