A. Askarov and A. Sabelfeld, Gradual Release: Unifying Declassification, Encryption and Key Release Policies (SP '07), pp.207-221, 2007.

G. Barthe, B. Grégoire, and V. Laporte, Secure compilation of side-channel countermeasures: the case of cryptographic "constant-time, Proc. of the 31st Computer Security Foundations Symposium, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01959560

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A Static Analyzer for Large Safety-critical Software, Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI '03), 2003.
URL : https://hal.archives-ouvertes.fr/hal-00128135

, , pp.196-207

S. Chong and A. C. Myers, Language-Based Information Erasure, Proceedings of the 18th IEEE Workshop on Computer Security Foundations (CSFW '05), pp.241-254, 2005.

S. Chong and A. C. Myers, End-to-End Enforcement of Erasure and Declassification, Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium (CSF '08), pp.98-111, 2008.

C. Deng and K. S. Namjoshi, Securing a Compiler Transformation, 23rd Int. Static Analysis Symposium, vol.9837, pp.170-188, 2016.

D. Vijay, M. Silva, D. Payer, and . Song, The Correctness-Security Gap in Compiler Optimization, Proc. of the 2015 IEEE Security and Privacy Workshops (SPW '15), pp.73-87, 2015.

L. George and A. W. Appel, Iterated Register Coalescing. ACM Trans. Program. Lang. Syst, vol.18, pp.300-324, 1996.

Y. Huang, B. R. Childers, and M. L. Soffa, Catching and Identifying Bugs in Register Allocation, Proceedings of the 13th International Conference on Static Analysis (SAS'06), pp.281-300, 2006.

S. Hunt and D. Sands, Just Forget It: The Semantics and Enforcement of Information Erasure, Proceedings of the Theory and Practice of Software, 17th European Conference on Programming Languages and Systems (ESOP'08/ETAPS'08), pp.239-253, 2008.

I. , , 2011.

B. Jacobs, J. Smans, and P. Philippaerts, VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, Proc. of the 3d Int. Symp. on NASA Formal Methods, vol.6617, pp.41-55, 2011.

X. Leroy, Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant, Conference Record of the 33rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL '06), pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

X. Leroy, Formal verification of a realistic compiler, Commun. ACM, vol.52, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

F. Nielson, R. Hanne, C. Nielson, and . Hankin, Principles of Program Analysis, 1999.
DOI : 10.1007/978-3-662-03811-6
URL : http://www.seas.harvard.edu/courses/cs252/2011sp/slides/Lec11-AbstractInt.pdf

A. Pnueli, M. Siegel, and E. Singerman, Translation Validation, Tools and Algorithms for Construction and Analysis of Systems (LNCS), vol.1384, pp.151-166, 1998.

S. Rideau and X. Leroy, Validating Register Allocation and Spilling, Proceedings of the 19th Joint European Conference on Theory and Practice of Software, International Conference on Compiler Construction (CC'10/ETAPS'10), pp.224-243, 2010.
DOI : 10.1007/978-3-642-11970-5_13
URL : https://hal.archives-ouvertes.fr/inria-00529841

A. Sabelfeld and D. Sands, Declassification: Dimensions and principles, Journal of Computer Security, vol.17, pp.517-548, 2009.
DOI : 10.3233/jcs-2009-0352
URL : http://www.md.chalmers.se/~andrei/sabelfeld-sands-jcs07.pdf

L. Simon, D. Chisnall, and R. Anderson, What you get is what you C: Controlling side effects in mainstream C compilers, 3rd IEEE European Symposium on Security and Privacy (EuroSP), 2018.
DOI : 10.1109/eurosp.2018.00009

Y. Tan, M. O. Myreen, R. Kumar, A. Fox, S. Owens et al., A New Verified Compiler Backend for CakeML, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, pp.60-73, 2016.
DOI : 10.1145/3022670.2951924
URL : http://kar.kent.ac.uk/55687/7/paper.pdf

X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich et al., Undefined Behavior: What Happened to My Code, Proceedings of the Third ACM SIGOPS Asia-Pacific Conference on Systems (APSys '12). USENIX Association, pp.9-9, 2012.
DOI : 10.1145/2349896.2349905
URL : http://dspace.mit.edu/bitstream/1721.1/86949/1/Kaashoek_Undefined%20behavior.pdf

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and Understanding, Bugs in C Compilers. SIGPLAN Not, vol.46, issue.6, pp.283-294, 2011.

Z. Yang, B. Johannesmeyer, A. T. Olesen, S. Lerner, and K. Levchenko, Dead Store Elimination (Still) Considered Harmful, Proceedings of the 26th USENIX Conference on Security Symposium (SEC'17). USENIX Association, pp.1025-1040, 2017.