A. Albert, P. Arenas, S. Genaim, M. Gómez-zamalloa, G. Puebla et al., Termination and Cost Analysis with COSTA and its User Interfaces, Electronic Notes in Theoretical Computer Science, vol.258, issue.1, p.???????
DOI : 10.1016/j.entcs.2009.12.008

URL : http://doi.org/10.1016/j.entcs.2009.12.008

G. Balakrishnan, T. Reps, D. Melski, and T. Teitelbaum, ????????: What You See Is Not What You eXecute, p.???????

S. Blazy and X. Leroy, Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning ??.? (????), p.pp. ???????
DOI : 10.1007/s10817-009-9148-3

URL : https://hal.archives-ouvertes.fr/inria-00352524

F. Bourdoncle, Efficient chaotic iteration strategies with widenings, Proc. of the Int. Conf. on Formal Methods in Programming and Their Applications, p.pp. ???????
DOI : 10.1007/BFb0039704

H. Bpf??-]-sébastien-bardin, V. Philippe, and . Frank, Refinement-based CFG Reconstruction from Unstructured Programs

. Br??-]-g, T. Balakrishnan, and . Reps, WYSINWYX: What you see is not what you eXecute, In: ACM Trans. Program. Lang. Syst. ??.? (????), p.pp. ????

A. Balakrishnan and C. Schulze, Code Obfuscation Literature Survey. Tech. rep. CS??? Construction of Compilers

P. Cousot and R. Cousot, Basic Concepts of Abstract Interpretation, Building the Information Society, p.???????
DOI : 10.1007/978-1-4020-8157-6_27

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, p.pp. ???????
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/inria-00528590

S. K. Coo+??-]-kevin-coogan, T. Debray, G. M. Kaochar, and . Townsend, Automatic Static Unpacking of Malware Binaries, p.???????

D. Cachera and D. Pichardie, A Certified Denotational Abstract Interpreter, Proc. of Int. Conf. on Interactive Theorem Proving, p.pp. ????
DOI : 10.1007/978-3-642-14052-5_3

URL : https://hal.archives-ouvertes.fr/inria-00537810

C. Ctl??-]-christian-collberg, D. Thomborson, and . Low, A Taxonomy of Obfuscating Transformations

A. [. Guillot and . Gazet, Désobfuscation automatique de binaire-The Barbarian Sublimation

[. Kruegel, W. Robertson, F. Valeur, and G. Vigna, Static disassembly of obfuscated binaries, Proceedings of USENIX Security. ????, p.???????

J. Kinder and H. Veith, Precise Static Analysis of Untrusted Driver Binaries, p.?????

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, p.pp. ?? ??
DOI : 10.1007/s10817-008-9099-0

URL : https://hal.archives-ouvertes.fr/inria-00289542

C. Linn and S. Debray, Obfuscation of executable code to improve resistance to static disassembly, Proceedings of the 10th ACM conference on Computer and communication security , CCS '03, p.pp. ???????
DOI : 10.1145/948109.948149

X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the ??rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL '??, p.pp. ?????
URL : https://hal.archives-ouvertes.fr/inria-00000963

S. Lescuyer, Conteneurs de première classe en Coq In: Journées Francophones des Langages Applicatifs (????) ???

J. Lim, Transformer specification language: a system for generating analyzers and its applications

]. M. Mad+??, B. Madou, B. Anckaert, K. De-bus, J. De-bosschere et al., On the effectiveness of source code transformations for binary obfuscation

L. Mauborgne, ASTRÉE: Verification of Absence of Run-Time Error " . In: Building the information Society (??th IFIP World Computer Congress), p.pp. ???????

[. Madou, L. Van-put, and K. De-bosschere, LOCO, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation , PEPM '06, p.pp. ???????
DOI : 10.1145/1111542.1111566

. F. Nnh??, H. R. Nielson, C. Nielson, and . Hankin, Principles of program analysis

[. Popov, S. Debray, and G. Andrews, Binary Obfuscation Using Signals, Proc. Usenix Security. ????, p.???????

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

[. Reps, G. Balakrishnan, and J. Lim, Intermediate-representation recovery from low-level code, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation , PEPM '06
DOI : 10.1145/1111542.1111560

. Rep+??, J. Thomas-reps, A. Lim, G. Thakur, A. Balakrishnan et al., There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code, Computer Aided Verification, p.?????

B. [. Roundy and . Miller, Hybrid Analysis and Control of Malware, In: RAID. Sept. ????, p.???????
DOI : 10.1007/978-3-642-15512-3_17

M. Sozeau and N. Oury, First-Class Type Classes, Theorem Proving in Higher Order Logics (????), p.pp. ???????
DOI : 10.1007/11542384_8

URL : https://hal.archives-ouvertes.fr/inria-00628864

K. Udm??-]-sharath, S. K. Udupa, M. Debray, and . Madou, Deobfuscation: Reverse Engineering Obfuscated Code

[. Wang, J. Hill, J. Knight, and J. Davidson, Software Tamper Resistance: Obstructing Static Analysis of Programs

]. H. War?? and . Warren-jr, Hacker's Delight