D. Beyer, Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016), p.887904, 2016.
DOI : 10.1007/978-3-662-49674-9_55

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00528442

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.
DOI : 10.1145/780822.781153

URL : https://hal.archives-ouvertes.fr/hal-00128135

B. Y. Chang and K. R. Leino, Abstract Interpretation with Alien Expressions and Heap Structures, p.147163, 2005.
DOI : 10.1007/978-3-540-30579-8_11

B. Y. Chang and X. Rival, Modular Construction of Shape-Numeric Analyzers, Festschrift for Dave Schmidt. Festschrift for Dave Schmidt, 2013.
DOI : 10.1007/3-540-61739-6_53

URL : https://hal.archives-ouvertes.fr/hal-00926948

A. Costan, S. Gaubert, E. Goubault, M. Martel, and S. Putot, A policy iteration algorithm for computing xed points in static analysis of programs, Computer aided verication, p.462475, 2005.

P. Cousot and R. Cousot, Abstract interpretation: a unied lattice model for static analysis of programs by construction or approximation of xpoints, Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p.238252, 1977.

P. Cousot and R. Cousot, Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, p.511547, 1992.
DOI : 10.1093/logcom/2.4.511

P. Cousot, R. Cousot, and F. Logozzo, A parametric segmentation functor for fully automatic and scalable array content analysis, Conference Record of the 38 th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011.
DOI : 10.1145/1926385.1926399

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

R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck, Eciently computing static single assignment form and the control dependence graph, ACM Trans. Program. Lang. Syst, vol.13, issue.4, p.451490, 1991.
DOI : 10.1145/115372.115320

A. Djoudi, S. Bardin, and É. Goubault, Recovering High-Level Conditions from Binary Programs, FM 2016: Formal Methods -21st International Symposium Proceedings, p.235253, 2016.
DOI : 10.1109/SP.2015.47

M. Fähndrich and F. Logozzo, Static Contract Checking with Abstract Interpretation, Proceedings of the 2010 International Conference on Formal Verication of Object-oriented Software. pp. 1030. FoVeOOS'10, 2011.
DOI : 10.1007/978-3-540-79124-9_10

G. Gange, J. A. Navas, P. Schachte, H. Søndergaard, and P. J. Stuckey, An Abstract Domain of Uninterpreted Functions, p.85103, 2016.
DOI : 10.1007/978-3-662-49122-5_4

G. Gange, J. A. Navas, P. Schachte, H. Søndergaard, and P. J. Stuckey, Exploiting sparsity in dierence-bound matrices, Proceedings of the 23rd Static Analysis Symposium, 2016.
DOI : 10.1007/978-3-662-53413-7_10

L. Gonnord and P. Schrammel, Abstract acceleration in linear relation analysis, Science of Computer Programming, vol.93, p.125153, 2014.
DOI : 10.1016/j.scico.2013.09.016

URL : https://hal.archives-ouvertes.fr/hal-00785116

P. Granger, Static analysis of arithmetical congruences, International Journal of Computer Mathematics, vol.30, issue.3-4, p.165190, 1989.
DOI : 10.1145/29873.29875

J. H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formallyveried c static analyzer, ACM SIGPLAN Notices, vol.50, issue.1, p.247259, 2015.
DOI : 10.1145/2775051.2676966

M. Karr, Ane relationships among variables of a program, Acta Informatica, vol.6, p.133151, 1976.

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective, Formal Aspects of Computing, vol.12, issue.1???2, p.573609, 2015.
DOI : 10.1007/11408901_21

K. Leino, Ecient weakest preconditions, Information Processing Letters, vol.93, issue.6, p.281288, 2005.
DOI : 10.1016/j.ipl.2004.10.015

URL : http://research.microsoft.com/pubs/70052/tr-2004-34.pdf

F. Logozzo and M. Fähndrich, On the Relative Completeness of Bytecode Analysis Versus Source Code Analysis, 2008.
DOI : 10.1007/978-3-540-78791-4_14

A. K. Mackworth, Consistency in networks of relations, Artificial Intelligence, vol.8, issue.1, pp.99-118, 1977.
DOI : 10.1016/0004-3702(77)90007-8

A. Miné, Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, Proc. of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES'06, 2006.

A. Miné, Symbolic Methods to Enhance the Precision of Numerical Abstract Domains, 2007.
DOI : 10.1007/11609773_23

F. Nielson, H. R. Nielson, and C. 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

H. Oh, K. Heo, W. Lee, W. Lee, and K. Yi, Design and implementation of sparse global analyses for c-like languages, Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation . pp. 229238. PLDI '12, 2012.

S. De-oliveira, S. Bensalem, and V. Prevosto, Polynomial Invariants by Linear Algebra, Automated Technology for Verication and Analysis -14th International Symposium, ATVA 2016 Proceedings, p.479494, 2016.
DOI : 10.1137/0201010

G. Plotkin, A structural approach to operational semantics, Tech. rep, 1981.

A. Venet and G. P. Brat, Precise and ecient static array bound checking for large embedded C programs, Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, p.231242, 2004.
DOI : 10.1145/996893.996869

URL : http://www.ic.arc.nasa.gov/m/pub/753h/0753%20(Venet).pdf

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, 1994.
DOI : 10.1006/inco.1994.1093

URL : https://doi.org/10.1006/inco.1994.1093