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

A. W. Appel, Modern Compiler Implementation in ML, 1998.

Y. Bertot, Structural abstract interpretation, a formal study in Coq, Language Engineering and Rigorous Software Development, pp.153-194, 2009.

F. Besson, D. Cachera, T. P. Jensen, and D. Pichardie, Certified static analysis by abstract interpretation, Foundations of Security Analysis and Design, pp.223-257, 2009.
DOI : 10.1007/978-3-642-03829-7_8
URL : https://hal.archives-ouvertes.fr/inria-00538753

F. Besson, T. Jensen, and D. Pichardie, Proof-carrying code from certified abstract interpretation to fixpoint compression, Theoretical Computer Science, vol.364, issue.3, pp.273-291, 2006.

P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Programming Language Implementation and Logic Programming, pp.269-295, 1992.

F. Dabrowski and D. Pichardie, A certified data race analysis for a Java-like language, 22nd International Conference on Theorem Proving in Higher Order Logics, pp.212-227, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00465547

M. Hind, Pointer analysis: haven't we solved this problem yet? In: Program Analysis For Software Tools and Engineering (PASTE'01), pp.54-61, 2001.

G. A. Kildall, A unified approach to global program optimization In: 1st symposium Principles of Programming Languages, pp.194-206, 1973.

J. R. Larus and P. N. Hilfinger, Detecting conflicts between structure accesses, Programming Language Design and Implementation (PLDI'88, pp.21-34, 1988.
DOI : 10.1145/960116.53993

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

X. Leroy, A formally verified compiler back-end, J. Automated Reasoning, vol.43, issue.4, pp.363-446, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00360768

X. Leroy, A. W. Appel, S. Blazy, and G. Stewart, The CompCert memory model, version 2, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00703441

X. Leroy and S. Blazy, Formal verification of a C-like memory model and its uses for verifying program transformations, J. Automated Reasoning, vol.41, issue.1, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00289542

T. Nipkow, Abstract interpretation of annotated commands, Interactive Theorem Proving, pp.116-132, 2012.

B. Steensgaard, Points-to analysis in almost linear time, 23rd symp. Principles of Programming Languages (POPL'96, pp.32-41, 1996.