. [. Bibliography, E. Annichini, A. Asarin, and . Bouajjani, Symbolic techniques for parametric reasoning about counter and clock systems, CAV'00, pp.419-449, 2001.

G. Ameur, F. Bel, S. Boniol, V. Pairault, and . Wiels, Robustness analysis of avionics embedded systems, ACM LCTES'03, pp.123-132

[. Ameur, P. Cros, J. Falcón, and A. Gómez, An application of abstract interpretation to floating-point arithmetic, WSA'92, pp.205-212

J. [. Aho, J. Hopcroft, and . Ullman, The Design and Analysis of Computer Algorithms, 1974.

. Astrée, Analyse Statique de logiciels Temps-R ´ Eel embarqués (static analysis of critical real-time embedded software) analyzer page

. Astrée, Analyse Statique de logiciels Temps-R ´ Eel embarqués (static analysis of critical real-time embedded software) RNTL project page

]. R. Bag97 and . Bagnara, Data-Flow Analysis for Constraint Logic-Based Languages, Corso ItaliaPapers, vol.40, 1997.

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, Antoine Miné Weakly Relational Numerical Abstract Domains The Essence of Computation: Complexity, Analysis, Transformation . Essays Dedicated to Neil D. Jones, pp.85-108, 2002.

]. B. Bcc-+-03, P. Blanchet, R. Cousot, J. Cousot, L. Feret et al., A static analyzer for large safety-critical software, ACM PLDI'03, pp.196-207, 2003.

]. R. Bel58 and . Bellman, On a routing problem, In Quarterly of Applied Mathematics, vol.16, pp.87-90, 1958.

P. [. Bagnara, E. Hill, E. Ricci, and . Zaffanella, Precise widening operators for convex polyhedra, SAS'03, pp.337-354, 2003.
DOI : 10.1007/3-540-44898-5_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.7610

P. [. Bagnara, E. Hill, and . Zaffanella, Widening operators for powerset domains, VMCAI'04, pp.135-148, 2003.
DOI : 10.1007/s10009-007-0029-y
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.219

K. [. Balasundaram and . Kennedy, A technique for summarizing data access and its use in parallelism enhancing transformations, ACM PLDI'89, pp.41-53, 1989.

]. F. Bou90 and . Bourdoncle, Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity, PLILP'90, pp.307-323, 1990.

]. F. Bou93a and . Bourdoncle, Abstract debugging of higher-order imperative languages, ACM PLDI'93, pp.46-55, 1993.

]. F. Bou93b and . Bourdoncle, Efficient chaotic iteration strategies with widenings, FMPA'93, pp.128-142, 1993.

]. R. Bry86 and . Bryant, Graph-based algorithms for Boolean function manipulation, Domaines numériques abstraits faiblement relationnels Antoine Miné, pp.35677-691, 1986.

E. [. Bagnara, E. Ricci, P. M. Zaffanella, and . Hill, Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library, SAS'02, pp.213-229, 2002.
DOI : 10.1007/3-540-45789-5_17

]. L. Car97 and . Cardelli, Type systems, The Computer Science and Engineering Handbook, 1997.

R. [. Cousot and . Cousot, Static determination of dynamic properties of programs, pp.106-130, 1976.

R. [. Cousot and . 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

R. [. Cousot and . 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. Cc92a, R. Cousot, and . Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, vol.13, issue.23, pp.103-179, 1992.

]. P. Cc92b, R. Cousot, and . Cousot, Abstract interpretation frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.

]. P. Cc92c, R. Cousot, and . Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper, PLILP'92, pp.269-295, 1992.

R. [. Cousot and . Cousot, Modular static program analysis, invited paper, CC'02, pp.159-178, 2002.

J. [. Clarisó and . Cortadella, The octahedron abstract domain, SAS'04, pp.312-327, 2004.

. Cea and . Cea, Fluctuat: a static analyzer for floating-point operations. http://wwwdrt .cea.fr/Pages

O. [. Clarke and D. A. Grumberg, Peled. Model Checking, 2000.

N. [. Cousot and . 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

C. [. Cormen, R. Leiserson, and . Rivest, Introduction to Algorithms, 1990.

]. C. Col96 and . Colby, Semantics-Based Program Analysis via Symbolic Composition of Transfer Relations, 1996.

]. P. Cou78 and . 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, Thèse d'´ etatèsetatès sciences mathématiques, 1978.

]. P. Cou99 and . Cousot, The calculational design of a generic abstract interpreter, Calculational System Design. NATO ASI Series F. IOS Press, 1999.

]. P. Cou02 and . Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, vol.277, issue.12, pp.47-103, 2002.

]. P. Cou03 and . Cousot, Verification by abstract interpretation on Verification ? Theory & Practice ? Honoring Zohar Manna's 64th Birthday, Proc. Int. Symp, pp.243-268, 2003.

A. /. Ieee, IEEE standard for binary floating-point arithmetic, 1985.

. A. Domaines-numériques-abstraits-faiblement-relationnels-antoine-miné-[-cs01-]-m, H. B. Colón, and . Sipma, Synthesis of linear ranking functions, TACAS'01, pp.67-81, 2001.

]. A. Deu94 and . Deutsch, Interprocedural may-alias analysis for pointers: Beyond klimiting, ACM PLDI'94, pp.230-241, 1994.

M. [. Dor, M. Rodeh, and . Sagiv, Cleanness Checking of String Manipulations in C Programs via Integer Analysis, SAS'01, 2001.
DOI : 10.1007/3-540-47764-0_12

]. J. Fer01 and . Feret, Occurrence counting analysis for the ?-calculus. GETCO'00, 2001.

]. J. Fer04a and . Feret, Abstract interpretation of mobile systems, JLAP, 2004.

]. J. Fer04b and . Feret, Static analysis of digital filters, LNCS, vol.2986, 2004.

]. J. Fer05 and . Feret, The arithmetic-geometric progression abstract domain, VM- CAI'05, 2005.

]. J. Ga and . Garrigue, LablGTK2: an interface to the GIMP Tool Kit

D. Gopan, F. Dimaio, N. Dor, T. Reps, and M. Sagiv, Numeric Domains with Summarized Dimensions, TACAS'04, pp.512-529, 2004.
DOI : 10.1007/978-3-540-24730-2_38
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8931

]. D. Ggp-+-01, ´. E. Guilbaud, A. Goubault, B. Pascalet, F. Starynkévitch et al., A simple abstract interpreter for threat detection and test case generation, WAPATV'01 in ICSE'01, 2001.

M. [. Gondran and . Minoux, Graphs and Algorithms, 1984.
URL : https://hal.archives-ouvertes.fr/hal-01304880

]. D. Gol91 and . Goldberg, What every computer scientist should know about floatingpoint arithmetic, ACM Computing Surveys (CSUR), vol.23, issue.1, pp.5-48, 1991.

[. Goubault, Static Analyses of the Precision of Floating-Point Operations, SAS'01, pp.234-259, 2001.
DOI : 10.1007/3-540-47764-0_14

]. P. Gra89 and . Granger, Static analysis of arithmetical congruences, In International Journal of Computer Mathematics, vol.30, pp.165-190, 1989.

]. P. Gra91 and . Granger, Static analysis of linear congruence equalities among variables of a program, TAPSOFT'91, pp.169-192, 1991.

]. P. Gra92 and . Granger, Improving the results of static analyses programs by local decreasing iteration, FSTTCS, pp.68-79, 1992.

]. P. Gra97 and . Granger, Static analyses of congruence properties on rational numbers, SAS'97, pp.278-292, 1997.

]. N. Hal79 and . Halbwachs, Détermination automatique de relations linéaires vérifiés par les variables d'un programme, 1979.

]. E. Han75 and . Hansen, A generalized interval arithmetic, Interval Mathematics, pp.7-18, 1975.

P. [. Harvey and . Stuckey, A unit two variable per inequality integer constraint solver for constraint logic programming, ACSC'97, pp.102-111, 1997.

S. [. Handjieva and . Tzolovski, Refining Static Analyses by Trace-Based Partitioning Using Control Flow, SAS'98, pp.200-214, 1998.
DOI : 10.1007/3-540-49727-7_12

]. B. Jea and . Jeannet, New polka: A library to handle convex polyhedra in any dimension

J. Jaffar, M. Maher, P. Stuckey, and H. Yap, Beyond finite domains, PPCP'94, pp.86-94, 1994.
DOI : 10.1007/3-540-58601-6_92

]. M. Kar76 and . Karr, Affine relationships among variables of a program, Acta Informatica, pp.133-151, 1976.

]. G. Kil73 and . Kildall, A unified approach to global program optimization, ACM POPL'73, pp.194-206, 1973.

F. [. Larsen, P. Larsson, W. Pettersson, and . Yi, Efficient verification of realtime systems: Compact data structure and state-space reduction, IEEE RTSS'97, pp.14-24, 1997.

[. Verge, A note on Chernikova's algorithm, 1992.

C. [. Larsen, W. Weise, J. Yi, and . Pearson, Clock Difference Diagrams, BRICS Report Series, vol.5, issue.46, pp.271-298, 1999.
DOI : 10.7146/brics.v5i46.19491
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.1868

]. M. Mal71 and . Malcolm, On accurate floating-point summation, Commun. ACM, vol.14, issue.11, pp.731-736, 1971.

]. E. Man92 and . Manes, Predicate Transformer Semantics, 1992.

]. M. Mar02a and . Martel, Propagation of rounding errors in finite precision computations: A semantics approach, ESOP'02, pp.194-208

]. M. Mar02b and . Martel, Static analysis of the numerical stability of loops, SAS'02, pp.133-150, 2002.

]. F. Mas92 and . Masdupuy, Array abstraction using semantic analysis of trapezoid congruences, ACM ICS'92, pp.226-235, 1992.

F. Masdupuy, Semantic analysis of interval congruences, FMPTA'93, pp.142-155, 1993.
DOI : 10.1007/BFb0039705

]. I. Mas01 and . Mastroeni, Numerical power analysis, PADO II, pp.117-137, 2001.

]. L. Mau99 and . Mauborgne, Representation of Sets of Trees for Abstract Interpretation, 1999.

]. L. Mau04 and . Mauborgne, ASTRÉEASTR´ASTRÉE: verification of absence of run-time error, Building the Information Society, pp.385-392, 2004.

B. [. Measche and . Berthomieu, Time petri-nets for analyzing and verifying time dependent communication protocols. Protocol Specification, Testing and Verification III, pp.161-172, 1983.

]. A. Mina and . Miné, The octagon abstract domain library

]. A. Minb and . Miné, On-line octagon abstract domain sample analyzer

]. A. Min00, D. E. Miné, . Report, . Univ, and V. Paris, Representation of two-variable difference or sum constraint set and application to automatic program analysis, 2000.

]. A. Min01a and . Miné, A new numerical abstract domain based on difference-bound matrices, PADO II, pp.155-172, 2001.

]. A. Min01b and . Miné, The octagon abstract domain, AST, pp.310-319, 2001.

]. A. Min02 and . Miné, A few graph-based relational numerical abstract domains, SAS'02, pp.117-132, 2002.

N. [. Muchnick and . Jones, Program Flow Analysis: Theory and Applications, 1981.

J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard, Difference Decision Diagrams, CSL'99, pp.111-125, 1999.
DOI : 10.1007/3-540-48168-0_9

]. D. Mona and . Monniaux, C99-compatible c front-end for ocaml

]. D. Monb and . Monniaux, Caml-gmp, an extended precision computation library

]. D. Mon01 and . Monniaux, An abstract Monte-Carlo method for the analysis of probabilistic programs, ACM POPL'01, pp.93-101, 2001.

]. R. Moo66 and . Moore, Interval Analysis, 1966.

. Mpf and . Mpfr, The multiple precision floating-point reliable library

]. C. Nel78 and . Nelson, An n logn algorithm for the two-variable-per-constraint linear programming satisfiability problem, 1978.

. Oca and . Ocaml, The objective caml system

. Ppl and . Ppl, The Parma Polyhedra Library

]. V. Pra77 and . Pratt, Two easy theories whose combination is hard, Massachusetts Institute of Technology. Cambridge, 1977.

]. Proa and . Project, Gcc: the GNU compiler collection

]. Prob and . Project, GTK+: the GIMP Tool Kit, version 2

E. Rodríguez-carbonell and D. Kapur, Automatic generation of polynomial loop invariants: Algebraic foundations, ACM ISSAC'04, pp.266-273, 2004.

]. J. [-rey69 and . Reynolds, Automatic computation of data set definitions. Information Processing'68, pp.456-461, 1969.

]. H. Ric53 and . Rice, Classes of recursively enumerable sets and their decision problems, In Trans. Amer. Math. Soc, vol.74, pp.358-366, 1953.

]. R. Rug04 and . Rugina, Quantitative shape analysis, SAS'04, pp.228-245, 2004.

]. R. Sho81 and . Shostak, Deciding linear inequalities by computing loop residues, Journal of the ACM, vol.28, issue.4, pp.769-779, 1981.

A. [. Simon and . King, Analyzing String Buffers in C, ICAMST, pp.365-379, 1367.
DOI : 10.1007/3-540-45719-4_25

]. R. Ske92 and . Skeel, Roundoff error and the Patriot missile, SIAM News, vol.25, issue.411, 1992.

. A. Skh02, A. Simon, J. King, and . Howe, Two variables per linear inequality as an abstract domain, LOPSTR'02, pp.71-89, 1515.

E. [. Shaham, M. Kolodner, and . Sagiv, Automatic Removal of Array Memory Leaks in Java, CC'00, pp.50-66, 2000.
DOI : 10.1007/3-540-46423-9_4

D. [. Su and . Wagner, A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings, TACAS'04, pp.280-295, 2004.
DOI : 10.1007/978-3-540-24730-2_23

J. [. Toman, D. S. Chomicki, and . Rogers, Datalog with integer periodicity constraints, Journal of Logic Programming, pp.189-203, 1994.
DOI : 10.1016/S0743-1066(97)10008-5
URL : http://doi.org/10.1016/s0743-1066(97)10008-5

M. Vinícius, A. Andrade, J. L. Comba, and J. Stolfi, Affine arithmetic, INTERVAL'94, 1994.

]. A. Ven02 and . Venet, Nonuniform alias analysis of recursive data structures and arrays, SAS'02, pp.36-51, 2002.

]. J. Vig96 and . Vignes, A stochastic approach of the analysis of round-off error propagation: A survey of the CESTAC method, Proc. of the Second Real Numbers and Computer Conf, pp.233-251, 1996.

]. S. Yov98 and . Yovine, Model-checking timed automata, Embedded Systems, 1998.

.. Abstract-test-on-zones, 84 3.10 Example of infinite increasing chain defined by m i+1 def = (m * i ) ? Zone std n i, p.91

I. Floyd, ?. Warshall-algorithm, .. {|-v-f-?-?-|-}-zone, and .. , 67 3.4.2 Intersection abstractions, p.76

?. Canonical-?, 9 2.2.2 Relative precision of abstract domains 13 2.2.4 Tarskian fixpoint transfer, 14 2.2.6 Kleenian iterations in domains with no infinite increasing chain. . . . 15 2.2.7 Fixpoint approximation with widening . 17 2.2.9 Chaotic iterations with widening. . . . . . . . . . . . . . . . . . . . . 18 2.2.10 Chaotic iterations with narrowing

?. Floyd and .. Warshall-algorithm-properties, 60 3.3.6 Local characterisation of closed matrices 64 3.4.1 Equality testing, p.76

.. Relational-domain, 44 2.5.2 Computation not possible in a non-relational domain 44 2.5.3 Loop invariant not representable in a non-relational domain 45 2.5.4 Symbolic invariant not representable in a non-relational domain, Domaines numériques abstraits faiblement relationnels Antoine Miné List of Examples 2.5.1 Property not representable 45 3.7.1 Using the standard zone widening 3.7.2 Using the widening with thresholds, p.93