M. Clochard, J. Filliâtre, C. Marché, and A. Paskevich, Formalizing semantics with an automatic program verier, 6th Working Conference on Veried Software : Theories, Tools and Experiments (VSTTE), p.3751, 2014.

A. Dieumegard and M. Pantel, Vérication d'un générateur de code par génération d'annotations (short paper), Conférence en Ingénierie du Logiciel (CIEL), p.page (en ligne, 2012.

J. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, 26th International Conference on Computer Aided Verication, p.116, 2014.

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, ESOP, p.125128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

J. B. Jensen, N. Benton, and A. Kennedy, High-level separation logic for low-level code, SIGPLAN Not, vol.48, issue.1, p.301314, 2013.

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

M. O. Myreen, Veried just-in-time compiler on x86, SIGPLAN Not, vol.45, issue.1, p.107118, 2010.

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot : Reasoning with the awkward squad, Proceedings of ICFP'08, 2008.

A. Appendice and A. , Semantique du langage source | E_WhileEnd : forall cond m body. not beval m cond ? ceval m (Cwhile cond body) m | E_WhileLoop : forall mi mj mf cond body. beval mi cond ? ceval mi body mj ? ceval mj (Cwhile cond body) mf ? ceval mi (Cwhile cond body) mf A.2. Semantique du langage cible inductive transition (c: code) (msi msj: machine_state) = | trans_const : forall c p n. codeseq_at c p (iconst n) ? forall s m. transition c (VMS p s m) (VMS (p + 1) (push n s) m)