A. W. Appel and S. Blazy, Separation Logic for Small-Step cminor, 20th Int. Conference on Theorem Proving in Higher Order Logics, pp.5-21, 2007.
DOI : 10.1007/978-3-540-74591-4_3
URL : https://hal.archives-ouvertes.fr/inria-00165915

B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai et al., On the (im)possibility of obfuscating programs, CRYPTO '01: Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology, pp.1-18

S. Blazy and R. Giacobazzi, Towards a formally verified obfuscating compiler, SSP 2012 -2nd ACM SIGPLAN Software Security and Protection Workshop, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00762330

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, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End, FM 2006: Formal Methods, 14th International Symposium on, pp.460-475, 2006.
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401

C. Collberg, The tigress C diversifier/obfuscator, pp.2014-2015

C. Collberg and J. Nagra, Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection, 2009.

C. Collberg and C. Thomborson, Watermarking, tamper-proofing, and obfuscation - tools for software protection, IEEE Transactions on Software Engineering, vol.28, issue.8, pp.735-746, 2002.
DOI : 10.1109/TSE.2002.1027797

S. Drape, C. D. Thomborson, and A. Majumdar, Specifying Imperative Data Obfuscations, Information Security, 10th International Conference Proceedings, pp.299-314, 2007.
DOI : 10.1007/978-3-540-75496-1_20

P. Junod, J. Rinaldini, J. Wehrli, and J. Michielin, Obfuscator-LLVM -- Software Protection for the Masses, 2015 IEEE/ACM 1st International Workshop on Software Protection, pp.3-9, 2015.
DOI : 10.1109/SPRO.2015.10

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 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

X. Leroy, Mechanized Semantics for Compiler Verification, Programming Languages and Systems, 10th Asian Symposium, APLAS 2012, pp.386-388, 2012.
DOI : 10.1007/978-3-642-35182-2_27
URL : https://hal.archives-ouvertes.fr/hal-01079337

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

C. Liem, Y. X. Gu, and H. Johnson, A compiler-based infrastructure for software-protection, Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security , PLAS '08, pp.33-44, 2008.
DOI : 10.1145/1375696.1375702

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, pp.290-299, 2003.
DOI : 10.1145/948109.948149

C. Wang, A security architecture for survivability mechanisms, 2001.

T. A. Welch, A Technique for High-Performance Data Compression, Computer, vol.17, issue.6, pp.8-19, 1984.
DOI : 10.1109/MC.1984.1659158