D. Denning and P. Denning, Certification of programs for secure information flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977.
DOI : 10.1145/359636.359712

J. Goguen and J. Meseguer, Security Policies and Security Models, 1982 IEEE Symposium on Security and Privacy, 1982.
DOI : 10.1109/SP.1982.10014

D. Volpano, C. Irvine, and G. Smith, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2-3, pp.167-187, 1996.
DOI : 10.3233/JCS-1996-42-304

A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands, Termination-Insensitive Noninterference Leaks More Than Just a Bit, Computer Security -ESORICS Lecture Notes in Computer Science, vol.4, issue.3, 2008.
DOI : 10.3233/JCS-1996-42-304
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.140.573

A. Russo and A. Sabelfeld, Dynamic vs. Static Flow-Sensitive Security Analysis, 2010 23rd IEEE Computer Security Foundations Symposium, pp.186-199, 2010.
DOI : 10.1109/CSF.2010.20

S. Hunt and D. Sands, On Flow-Sensitive Security Types, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.79-90, 2006.
DOI : 10.1145/1111037.1111045
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.388.4867

L. Guernic, G. Banerjee, A. Jensen, T. Schmidt, and D. , Automata-Based Confidentiality Monitoring Advances in Computer Science-ASIAN, Secure Software and Related Issues, pp.75-89, 2006.

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

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

A. Sabelfeld and A. Myers, Language-Based Information-Flow Security. Selected Areas in Communications, IEEE Journal on, vol.21, issue.1, pp.5-19, 2003.
DOI : 10.1109/jsac.2002.806121
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.3979

T. Austin and C. Flanagan, Efficient purely-dynamic information flow analysis, ACM SIGPLAN Notices, vol.44, issue.8, pp.20-31, 2009.
DOI : 10.1145/1667209.1667223

M. Assaf, J. Signoles, F. Tronel, and E. Totel, Program Transformation for Non-interference Verification on Programs with Pointers, 2013.
DOI : 10.1007/978-3-642-33826-7_16
URL : https://hal.archives-ouvertes.fr/hal-00814671

D. Chandra and M. Franz, Fine-Grained Information Flow Analysis and Enforcement in a Java Virtual Machine, Twenty-Third Annual Computer Security Applications Conference (ACSAC 2007), pp.463-475, 2007.
DOI : 10.1109/ACSAC.2007.37

J. Ligatti, L. Bauer, and D. Walker, Edit automata: enforcement mechanisms for run-time security policies, International Journal of Information Security, vol.3, issue.1-2, pp.2-16, 2005.
DOI : 10.1007/s10207-004-0046-8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.114.6074

S. Moore and S. Chong, Static Analysis for Efficient Hybrid Information-Flow Control, 2011 IEEE 24th Computer Security Foundations Symposium, pp.2011-2035, 2011.
DOI : 10.1109/CSF.2011.17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.229.1581

T. H. Austin and C. Flanagan, Permissive dynamic information flow analysis, Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS '10, pp.1-12, 2010.
DOI : 10.1145/1814217.1814220
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.297.9422

A. Chudnov and D. Naumann, Information Flow Monitor Inlining, 2010 23rd IEEE Computer Security Foundations Symposium, pp.200-214, 2010.
DOI : 10.1109/CSF.2010.21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.153.6508

J. Magazinius, A. Russo, and A. Sabelfeld, On-the-fly Inlining of Dynamic Security Monitors, Computers & Security, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01054519

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Software Engineering and Formal Methods, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

P. Cuoq, V. Prevosto, and B. Yakobowski, Frama-C's Value Analysis Plug-in, 2012.

P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language, 2012.