P. Akritidis, M. Costa, M. Castro, and S. Hand, Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors, In SSYM, pp.51-66, 2009.

S. Ananian, The static single information form, 1999.

L. O. Andersen, Program Analysis and Specialization for the C Programming Language, 1994.

C. Bauer, A. Frink, and R. Kreckel, Introduction to the GiNaC Framework for Symbolic Computation within the C++ Programming Language, Journal of Symbolic Computation, vol.33, issue.1, pp.1-12, 2002.
DOI : 10.1006/jsco.2001.0494

W. Blume and R. Eigenmann, Symbolic range propagation, Proceedings of 9th International Parallel Processing Symposium, pp.357-363, 1994.
DOI : 10.1109/IPPS.1995.395956

R. Bodik, R. Gupta, and V. Sarkar, ABCD: eliminating array bounds checks on demand, PLDI, pp.321-333, 2000.

D. Brumley, D. X. Song, T. Cker-chiueh, R. Johnson, and H. Lin, RICH: Automatically protecting against integer-based vulnerabilities, NDSS. USENIX, 2007.

J. Choi, R. Cytron, and J. Ferrante, Automatic construction of sparse data flow evaluation graphs, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.55-66, 1991.
DOI : 10.1145/99583.99594

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

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-96, 1978.
DOI : 10.1145/512760.512770

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., Why does Astr??e scale up?, Formal Methods in System Design, vol.345, issue.1, pp.229-264, 2009.
DOI : 10.1007/s10703-009-0089-6

R. Cytron, J. Ferrante, B. Rosen, M. Wegman, and K. Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems, vol.13, issue.4, pp.451-490, 1991.
DOI : 10.1145/115372.115320

D. Dhurjati, S. Kowshik, and V. Adve, SAFECode: enforcing alias analysis for weakly typed languages, PLDI, pp.144-157, 2006.

W. Dietz, P. Li, J. Regehr, and V. Adve, Understanding Integer Overflow in C/C++, ICSE, pp.760-770, 2012.
DOI : 10.1145/2743019

J. Ferrante, J. Ottenstein, and D. Warren, The program dependence graph and its use in optimization, ACM Transactions on Programming Languages and Systems, vol.9, issue.3, pp.319-349, 1987.
DOI : 10.1145/24039.24041

P. Ferrara, F. Logozzo, and M. Fähndrich, Safer unsafe code for .NET, ACM SIGPLAN Notices, vol.43, issue.10, pp.329-346, 2008.
DOI : 10.1145/1449955.1449791

B. Hardekopf and C. Lin, The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code, PLDI, pp.290-299, 2007.

C. Lattner and V. S. Adve, LLVM: A compilation framework for lifelong program analysis & transformation, International Symposium on Code Generation and Optimization, 2004. CGO 2004., pp.75-88, 2004.
DOI : 10.1109/CGO.2004.1281665

F. Logozzo and M. Fähndrich, Pentagons, Proceedings of the 2008 ACM symposium on Applied computing , SAC '08, pp.796-80731, 2006.
DOI : 10.1145/1363686.1363736

A. Miné, Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions, Science of Computer Programming, vol.93, 2013.
DOI : 10.1016/j.scico.2013.09.014

S. Nagarakatte, J. Zhao, M. M. Martin, and S. Zdancewic, Softbound: Highly compatible and complete spatial memory safety for c, PLDI, pp.245-258, 2009.

F. Nielson, H. R. Nielson, and C. Hankin, Principles of program analysis, 2005.
DOI : 10.1007/978-3-662-03811-6

H. Oh, K. Heo, W. Lee, W. Lee, and K. Yi, Design and implementation of sparse global analyses for c-like languages, PLDI, pp.1-11, 2012.

A. A. Rimsa, M. D. Amorim, F. M. Pereira, and R. Bigonha, Efficient static checker for tainted variable attacks, Science of Computer Programming, vol.80, issue.1, pp.91-105, 2014.
DOI : 10.1016/j.scico.2013.03.012

R. E. Rodrigues, V. H. Campos, and F. M. Pereira, A fast and low-overhead technique to secure programs against integer overflows, Proceedings of the 2013 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), 2013.
DOI : 10.1109/CGO.2013.6494996

R. Rugina and M. C. Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, ACM Transactions on Programming Languages and Systems, vol.27, issue.2, pp.185-235, 2005.
DOI : 10.1145/1057387.1057388

E. J. Schwartz, T. Avgerinos, and D. Brumley, All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask), 2010 IEEE Symposium on Security and Privacy, pp.1-15, 2010.
DOI : 10.1109/SP.2010.26

K. Serebryany, D. Bruening, A. Potapenko, and D. Vyukov, Addresssanitizer: a fast address sanity checker, USENIX ATC, pp.28-28, 2012.

M. S. Simpson and R. K. Barua, MemSafe: Ensuring the Spatial and Temporal Memory Safety of C at Runtime, 2010 10th IEEE Working Conference on Source Code Analysis and Manipulation, pp.93-128, 2013.
DOI : 10.1109/SCAM.2010.15

D. Singh and W. J. Kaiser, The atom LEAP platform for energy-efficient embedded computing, 2010.

A. L. Tavares, B. Boissinot, F. M. Pereira, and F. Rastello, Parameterized Construction of Program Representations for Sparse Dataflow Analyses, Compiler Construction, pp.2-21, 2014.
DOI : 10.1007/978-3-642-54807-9_2
URL : https://hal.archives-ouvertes.fr/hal-00963590

F. Tip, A survey of program slicing techniques, 1994.

J. Von-ronne, A. Gampe, D. Niedzielski, and K. Psarris, Safe bounds check annotations, Concurrency and Computation: Practice and Experience, vol.12, issue.6, pp.41-57, 2009.
DOI : 10.1002/cpe.1341

M. Weiser, Program Slicing, ICSE, pp.439-449, 1981.
DOI : 10.1109/TSE.1984.5010248

J. Wilander and M. Kamkar, A comparison of publicly available tools for dynamic buffer overflow prevention, NDSS, pp.1-12, 2003.

J. Zhao, S. Nagarakatte, M. M. Martin, and S. Zdancewic, Formal verification of ssa-based optimizations for llvm, PLDI, pp.175-186, 2013.