G. Balakrishnan and T. W. Reps, WYSINWYX, ACM Transactions on Programming Languages and Systems, vol.32, issue.6, 2010.
DOI : 10.1145/1749608.1749612

S. Bardin, P. Herrmann, and F. Védrine, Refinement-Based CFG Reconstruction from Unstructured Programs, In: VMCAI. LNCS, vol.6538, pp.54-69, 2011.
DOI : 10.1007/978-3-642-14295-6_27

S. Blazy, Formal Verification of a C Value Analysis Based on Abstract Interpretation, In: SAS. LNCS, vol.7935, pp.324-344, 2013.
DOI : 10.1007/978-3-642-38856-9_18
URL : https://hal.archives-ouvertes.fr/hal-00812515

G. Bonfante, J. Y. Marion, and D. Reynaud-plantey, A Computability Perspective on Self-Modifying Programs, 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, pp.231-239, 2009.
DOI : 10.1109/SEFM.2009.25
URL : https://hal.archives-ouvertes.fr/inria-00433472

D. Cachera and D. Pichardie, A Certified Denotational Abstract Interpreter, Proc. of ITP-10, pp.9-24, 2010.
DOI : 10.1007/978-3-642-14052-5_3
URL : https://hal.archives-ouvertes.fr/inria-00537810

H. Cai, Z. Shao, and A. Vaynberg, Certified Self-Modifying Code, pp.66-77, 2007.

A. Chlipala, Mostly-automated verification of low-level programs in computational separation logic, 2011.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790

J. Jensen, N. Benton, and A. Kennedy, High-Level Separation Logic for Low-Level Code, 2013.

A. Kennedy, Coq, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, pp.13-24, 2013.
DOI : 10.1145/2505879.2505897
URL : https://hal.archives-ouvertes.fr/hal-01081548

J. Kinder, Towards Static Analysis of Virtualization-Obfuscated Binaries, 2012 19th Working Conference on Reverse Engineering, pp.61-70, 2012.
DOI : 10.1109/WCRE.2012.16

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811

G. Morrisett, RockSalt: better, faster, stronger SFI for the x86, PLDI. 2012, pp.395-404

M. O. Myreen, Verified just-in-time compiler on x86, pp.107-118, 2010.

T. Nipkow, Abstract Interpretation of Annotated Commands, Proc. of ITP-12, pp.116-132, 2012.
DOI : 10.1007/978-3-642-32347-8_9

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

G. Stewart, L. Beringer, and A. W. Appel, Verified heap theorem prover by paramodulation, In: ICFP. ACM, pp.3-14, 2012.