A. G. Stephenson-et-al and C. George, Mars Climate Orbiter mishap investigation boord phase I report, Marshall Space Flight Center, 1999.

M. Alt, F. C. , F. Martin, and R. Wilhelm, Cache behavior prediction by abstract interpretation, Proc. 3 rd Int. Symp. SAS '96, pp.24-26, 1145.
DOI : 10.1007/3-540-61739-6_33

A. National-standards-institute and . Inc, Standard for binary floating-point arithmetic, IEEE, vol.754754, 1985.

A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, Bounded Model Checking, Advances in Computers, vol.58, pp.118-149, 2003.
DOI : 10.1016/S0065-2458(03)58003-2

B. Blanchet, Security protocols: from linear to classical logic by abstract interpretation, Information Processing Letters, vol.95, issue.5, pp.473-479, 2005.
DOI : 10.1016/j.ipl.2005.05.011

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, invited chapter, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, pp.85-108, 2002.

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, Proc. ACM SIGPLAN '2003 Conf. PLDI, pp.196-207, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00128135

P. Cousot, Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes (in French) Thèse d'État ès sciences mathématiques, 1978.

P. Cousot, Types as abstract interpretations, invited paper, 24 th POPL, pp.316-331, 1997.

P. Cousot, Partial completeness of abstract fixpoint checking, invited paper, Proc. 4 th Int. Symp. SARA '2000, Horseshoe Bay, LNAI 1864, pp.1-25, 2000.

P. Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, vol.277, issue.1-2, pp.47-103, 2002.
DOI : 10.1016/S0304-3975(00)00313-3

P. Cousot and R. Cousot, Static determination of dynamic properties of programs, Proc. 2 nd Int. Symp. on Programming, pp.106-130, 1976.

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/inria-00528590

P. Cousot and R. Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '79, pp.269-282, 1979.
DOI : 10.1145/567752.567778

P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper, Proc. 4 th Int. Symp. on PLILP '92, pp.26-28, 1992.

P. Cousot and R. Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, pp.83-94, 1992.
DOI : 10.1145/143165.143184

P. Cousot and R. Cousot, Temporal abstract interpretation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.12-25, 2000.
DOI : 10.1145/325694.325699

P. Cousot and R. Cousot, Systematic design of program transformation frameworks by abstract interpretation, 29 th POPL, pp.178-190, 2002.

P. Cousot and R. Cousot, Parsing as abstract interpretation of grammar semantics, Theoretical Computer Science, vol.290, issue.1, pp.531-544, 2003.
DOI : 10.1016/S0304-3975(02)00034-8

P. Cousot and R. Cousot, Basic concepts of abstract interpretation, invited chapter, Building the Information Society, pp.359-366, 2004.

P. Cousot and R. Cousot, Grammar analysis and parsing by abstract interpretation, invited chapter, Program Analysis and Compilation, Theory and Practice: Essays dedicated to Reinhard Wilhelm, pp.178-203, 2006.

P. Cousot and R. Cousot, Bi-inductive structural semantics, Information and Computation, vol.207, issue.2, pp.258-283, 2009.
DOI : 10.1016/j.ic.2008.03.025

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRÉE analyser, Proc. 14 th ESOP '2005, pp.21-30, 2005.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., Varieties of static analyzers: A comparison with ASTRÉE, invited paper, Proc. 1 st TASE '07, pp.3-17, 2007.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., Combination of Abstractions in the ASTR??E Static Analyzer, 11 th ASIAN 06, pp.272-300, 2006.
DOI : 10.1007/978-3-540-24725-8_2

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

V. Danos, J. Feret, W. Fontana, and J. Krivine, Abstract Interpretation of Cellular Signalling Networks, Proc. 9 th Int. Conf. VMCAI 2008, pp.83-97, 2008.
DOI : 10.1007/978-3-540-78163-9_11
URL : https://hal.archives-ouvertes.fr/inria-00528352

C. Ferdinand, R. Heckmann, and R. Wilhelm, Analyzing the Worst-Case Execution Time by Abstract Interpretation of Executable Code, Automotive Software ? Connected Services in Mobile Networks, First Automotive Software Workshop, pp.1-14, 2004.
DOI : 10.1007/11823063_1

J. Feret, Static Analysis of Digital Filters, Proc. 30 th ESOP, pp.33-48, 2004.
DOI : 10.1007/978-3-540-24725-8_4
URL : https://hal.archives-ouvertes.fr/inria-00528447

J. Feret, The Arithmetic-Geometric Progression Abstract Domain, Proc. 6 th Int. Conf. VMCAI 2005, pp.42-58, 2005.
DOI : 10.1007/978-3-540-30579-8_3
URL : https://hal.archives-ouvertes.fr/inria-00528450

J. Feret, Numerical abstract domains for digital filters In 1 st Int, Work. on Numerical & Symbolic Abstract Domains, issue.05, 2005.

R. W. Floyd, Assigning meaning to programs, Proc. Symposium in Applied Mathematics, pp.19-32, 1967.

R. Giacobazzi and F. Ranzato, Completeness in abstract interpretation: A domain perspective, Proc. 6 th Int. Conf. AMAST '97, pp.231-245, 1997.
DOI : 10.1007/BFb0000474

D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-48, 1991.
DOI : 10.1145/103162.103163

J. R. Hauser, Handling floating-point exceptions in numeric programs, ACM Transactions on Programming Languages and Systems, vol.18, issue.2, pp.139-174, 1996.
DOI : 10.1145/227699.227701

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

C. B. Jones, The early search for tractable ways of reasoning about programs, IEEE Annals of the History of Computing, vol.25, issue.2, pp.26-49, 2003.
DOI : 10.1109/MAHC.2003.1203057

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system, documentation and user's manual (release 3.06), 2002.

J. L. Lions, ARIANE 5 flight 501 failure, report by the inquiry board, 1999.

C. Lomont, An analysis of the excel 65535 " bug, version 1.21, 2007.

L. Mauborgne, ASTRÉE: Verification of absence of run-time error, Building the Information Society, pp.385-392, 2004.

L. Mauborgne and X. , Trace Partitioning in Abstract Interpretation Based Static Analyzers, Proc. 14 th ESOP '2005, pp.5-20, 2005.
DOI : 10.1007/978-3-540-31987-0_2

A. Miné, Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, Proc. 30 th ESOP, pp.3-17, 2004.
DOI : 10.1007/978-3-540-24725-8_2

A. Miné, Weakly Relational Numerical Abstract Domains, Thèse de doctorat en informatique, École polytechnique, 2004.

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

A. Miné, The octagon abstract domain. Higher-Order and Symbolic Computation, pp.31-100, 2006.

A. Miné, Symbolic Methods to Enhance the Precision of Numerical Abstract Domains, Proc. 7 th Int. Conf. VMCAI 2006, pp.348-363, 2006.
DOI : 10.1007/11609773_23

D. Monniaux, The Parallel Implementation of the Astr??e Static Analyzer, Proc. 3 rd APLAS '2005, pp.86-96, 2005.
DOI : 10.1007/11575467_7

D. Monniaux, The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, 2008.
DOI : 10.1145/1353445.1353446
URL : https://hal.archives-ouvertes.fr/hal-00128124

P. Naur, Proof of algorithms by general snapshots, BIT, vol.1, issue.4, pp.310-316, 1966.
DOI : 10.1007/BF01966091

S. Perdrix, Quantum Entanglement Analysis Based on Abstract Interpretation, Proc. 15 th Int. Symp. SAS '08, pp.270-282, 2008.
DOI : 10.1007/978-3-540-69166-2_18

X. Rival and L. Mauborgne, The trace partitioning abstract domain, ACM Transactions on Programming Languages and Systems, vol.29, issue.5, 2007.
DOI : 10.1145/1275497.1275501

J. Serra, Morphological filtering: An overview, Signal Processing, vol.38, issue.1, pp.3-11, 1994.
DOI : 10.1016/0165-1684(94)90052-3

H. Wolpe, M. Blair, S. Obenski, and P. Bridickas, Gao/imtec-92-26 patriot missile software problem, Information Management and Technology Division, 1992.