D. Cachera, T. 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

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

A. Fouilhé, D. Monniaux, and M. Périn, Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra, Static Analysis -20th International Symposium, pp.345-365, 2013.
DOI : 10.1007/978-3-642-38856-9_19

P. Herms, C. Marché, and B. Monate, A Certified Multi-prover Verification Condition Generator, Verified Software: Theories, Tools, Experiments, pp.2-17, 2012.
DOI : 10.1007/3-540-48118-4_45
URL : https://hal.archives-ouvertes.fr/hal-00639977

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

D. Pichardie, Interprétation abstraite en logique intuitionniste: extraction d'analyseurs Java certifiés, 2005.