A. W. Appel, Verified software toolchain, Proc of ESOP 2011, pp.1-17, 2011.
DOI : 10.1007/978-3-642-19718-5_1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.186.2538

A. W. Appel and S. Blazy, Separation Logic for Small-Step cminor, Proc. of TPHOLs, pp.5-21, 2007.
DOI : 10.1007/978-3-540-74591-4_3
URL : https://hal.archives-ouvertes.fr/inria-00165915

Y. Bertot, B. Grégoire, and X. Leroy, A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis, Proc. of TYPES 2006, pp.66-81, 2006.
DOI : 10.1007/11617990_5
URL : https://hal.archives-ouvertes.fr/inria-00289549

F. Besson, T. Jensen, D. Pichardie, and T. Turpin, Certified Result Checking for Polyhedral Analysis of Bytecode Programs, Proc. of TGC 2010, pp.253-267, 2010.
DOI : 10.1007/978-3-642-15640-3_17
URL : https://hal.archives-ouvertes.fr/inria-00537816

S. Boldo, J. Jourdan, X. Leroy, and G. Melquiond, A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, 2013 IEEE 21st Symposium on Computer Arithmetic, 2013.
DOI : 10.1109/ARITH.2013.30
URL : https://hal.archives-ouvertes.fr/hal-00743090

F. Bourdoncle, Efficient chaotic iteration strategies with widenings, Proc. of FMPA 1993, pp.128-141, 1993.
DOI : 10.1007/BFb0039704

D. Cachera, T. P. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, issue.1, pp.56-78, 2005.
DOI : 10.1016/j.tcs.2005.06.004
URL : https://hal.archives-ouvertes.fr/inria-00564633

D. Cachera and D. Pichardie, A Certified Denotational Abstract Interpreter, Proc. of ITP-10, pp.9-24, 2010.
DOI : 10.1007/978-3-642-14052-5_3
URL : https://hal.archives-ouvertes.fr/inria-00537810

S. Coupet-grimal and W. Delobel, A Uniform and Certified Approach for Two Static Analyses, Proc. of TYPES 2004, pp.115-137, 2004.
DOI : 10.1007/11617990_8

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

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRE?? Analyzer, Proc. of ESOP 2005, pp.21-30, 2005.
DOI : 10.1007/978-3-540-31987-0_3

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-97, 1978.
DOI : 10.1145/512760.512770

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C -a software analysis perspective, Proc. of SEFM 2012 14. D.Pichardie. Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés, pp.233-247, 2005.

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, ASCM 2007, p.333, 2007.
DOI : 10.1007/978-3-540-87827-8_28

G. Gonthier, Engineering mathematics: the odd order theorem proof, Proc. of POPL'13, pp.1-2, 2013.

M. Hofmann, A. Karbyshev, and H. Seidl, Verifying a Local Generic Solver in Coq, Proc. of SAS'10, pp.340-355, 2010.
DOI : 10.1007/978-3-642-15769-1_21

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.
DOI : 10.1145/1743546.1743574

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
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 V. Robert, A formally-verified alias analysis, Proc. of CPP 2012, pp.11-26, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00773109

A. Miné, Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, Proc. of LCTES'06, pp.54-63, 2006.

J. Navas, P. Schachte, H. Søndergaard, and P. Stuckey, Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code, Proc. of APLAS 2012, 2012.
DOI : 10.1007/978-3-642-35182-2_9

T. Nipkow, Abstract Interpretation of Annotated Commands, Proc. of ITP'12, pp.116-132, 2012.
DOI : 10.1007/978-3-642-32347-8_9

S. Rideau and X. Leroy, Validating Register Allocation and Spilling, Proc. of CC 2010, pp.224-243, 2010.
DOI : 10.1007/978-3-642-11970-5_13
URL : https://hal.archives-ouvertes.fr/inria-00529841

A. Simon and A. King, Taming the Wrapping of Integer Arithmetic, Proc. of SAS, pp.121-136, 2007.
DOI : 10.1007/978-3-540-74061-2_8

V. Vafeiadis and F. Z. Nardelli, Verifying Fence Elimination Optimisations, Proc. of SAS'11, pp.146-162, 2011.
DOI : 10.1145/42190.42277
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.232.9669