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, LNCS, vol.6538, pp.54-69, 2011.
DOI : 10.1007/978-3-642-14295-6_27

Y. Bertot, Structural abstract interpretation, A formal study in Coq In: Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School, LNCS, vol.5520, pp.153-194, 2008.

Y. Bertot, B. Grégoire, and X. Leroy, A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis, In: TYPES. LNCS, vol.3839, pp.66-81, 2006.
DOI : 10.1007/11617990_5
URL : https://hal.archives-ouvertes.fr/inria-00289549

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

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

G. Bonfante, J. 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, In: Interactive Theorem Proving (ITP). LNCS, vol.6172, pp.9-24, 2010.
DOI : 10.1007/978-3-642-14052-5_3
URL : https://hal.archives-ouvertes.fr/inria-00537810

D. Cachera and D. Pichardie, Comparing Techniques for Certified Static Analysis, Proc. of the 1st NASA Formal Methods Symposium (NFM'09), pp.111-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00538772

D. Cachera, Extracting a data flow analyser in constructive logic, In: Theor. Comput. Sci, vol.3421, pp.56-78, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00564633

H. Cai, Z. Shao, and A. Vaynberg, Certified Self- Modifying Code, Conf. on Programming Language Design and Implementation (PLDI), pp.66-77, 2007.

A. Chlipala, Mostly-automated verification of low-level programs in computational separation logic, Conf. on Programming Language Design and Implementation (PLDI), 2011.

C. Collberg, C. Thomborson, and D. Low, Manufacturing cheap, resilient, and stealthy opaque constructs, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.184-196, 1998.
DOI : 10.1145/268946.268962
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.1946

S. Coupet-grimal and W. Delobel, A Uniform and Certified Approach for Two Static Analyses, In: TYPES. LNCS, vol.3839, pp.115-137, 2004.
DOI : 10.1007/11617990_8

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

K. Saumya, K. P. Debray, G. M. Coogan, and . Townsend, On the semantics of self-unpacking malware code, 2008.

R. T. Gerth, Formal Verification of Self Modifying Code, Int. Conf. for Young Computer Scientists. International Academic Publishers, China, 1991.

J. Jensen, N. Benton, and A. Kennedy, High-Level Separation Logic for Low-Level Code, Symp. on Principles of Programm. Lang. (POPL), 2013.

J. Jourdan, Formal verification of a C static analyzer, 42nd symposium Principles of Programming Languages (POPL). 2015, pp.247-259

A. Kennedy, Coq, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13
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
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

D. Monniaux, Réalisation mécanisée d'interpréteurs abstraits, 1998.

G. Morrisett, RockSalt: better, faster, stronger SFI for the x86, Conf. on Programming Language Design and Implementation (PLDI). 2012, pp.395-404

M. O. Myreen, Verified just-in-time compiler on x86, In: Symp. on Principles of Programm. Lang. (POPL, pp.107-118, 2010.

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

D. Pichardie, Building Certified Static Analysers by Modular Construction of Well-founded Lattices, Electronic Notes in Theoretical Computer Science, vol.212, pp.225-239, 2008.
DOI : 10.1016/j.entcs.2008.04.064
URL : https://hal.archives-ouvertes.fr/inria-00332365

D. Pichardie, Building Certified Static Analysers by Modular Construction of Well-founded Lattices, Proc. of the 1 st International Conference on Foundations of Informatics, Computing and Software (FICS), pp.225-239, 2008.
DOI : 10.1016/j.entcs.2008.04.064
URL : https://hal.archives-ouvertes.fr/inria-00332365

D. Pichardie, Interprétation abstraite en logique intuitionniste: extraction d'analyseurs Java certifiés, 2005.

V. Robert and X. Leroy, A Formally-Verified Alias Analysis, In: Certified Proofs and Programs (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: Int. Conf. on Functional Programming, pp.3-14, 2012.

P. Szor, The Art of Computer Virus Research and Defense, p.321304543, 2005.