. Bibliography, S. Xavier-allamigeon, E. Gaubert, and . Goubault, Inferring Min and Max Invariants Using Max-plus Polyhedra, Proceedings of the 15th International Static Analysis Symposium (SAS'08), pp.189-204, 2008.

[. Adjé, S. Gaubert, and E. Goubault, Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis, ESOP, pp.23-42, 2010.

[. Althoff, O. Stursberg, and M. Buss, Verification of Uncertain Embedded Systems by Computing Reachable Sets based on Zonotopes, IFAC World Congress, pp.5125-5130, 2008.
DOI : 10.3182/20080706-5-KR-1001.00861

. Astre, real-time embedded software static analyzer

[. Baumann, Optimal centered forms, BIT, vol.28, issue.1, pp.80-87, 1988.
DOI : 10.1007/BF01934696

O. Bouissou, E. Conquet, P. Cousot, R. Cousot, J. Feret et al., Space software validation using abstract interpretation, Proc. of the Int. Space System Engineering Conf., Data Systems in Aerospace (DA- SIA 2009), volume SP-669, pp.1-7, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00528590

]. J. Bcc-+-10, P. Bertrane, R. Cousot, J. Cousot, L. Feret et al., Static analysis and verification of aerospace software by abstract interpretation, AIAA Infotech@Aerospace, pp.1-38, 2010.

S. Boldo and J. Filliatre, Formal Verification of Floating-Point Programs, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.187-194, 2007.
DOI : 10.1109/ARITH.2007.20
URL : https://hal.archives-ouvertes.fr/hal-01174892

]. B. Bor99 and . Borchers, A C library for Semidefinite Programming, 1999.

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

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

S. A. Costan, E. Gaubert, M. Goubault, S. Martel, and . Putot, A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs, Computer Aided Verification, 2005.
DOI : 10.1007/11513988_46

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

W. Chuba and W. Miller, Quadratic convergence in interval arithmetic, part I, BIT, vol.12, issue.3, pp.284-290, 1972.
DOI : 10.1007/BF01932300

A. [. Chen, P. Miné, and . Cousot, A Sound Floating-Point Polyhedra Abstract Domain, Proc. of the Sixth Asian Symposium on Programming Languages and Systems (APLAS'08), pp.3-18, 2008.
DOI : 10.1007/3-540-45013-0_7
URL : https://hal.archives-ouvertes.fr/hal-00531567

A. [. Chen, J. Miné, P. Wang, and . Cousot, Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships, Proc. of the 16th Int. Static Analysis Symposium (SAS'09), pp.309-325, 2009.
DOI : 10.1007/0-387-32698-7_2
URL : https://hal.archives-ouvertes.fr/hal-00531564

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

[. Cousot, Iterative reduced product, 2005.

L. D. João, J. Comba, and . Stolfi, Affine arithmetic and its applications to computer graphics. SIBGRAPI'93, 1993.

C. Q. Florent-de-dinechin, G. Lauter, and . Melquiond, Assisted verification of elementary functions using gappa, Proceedings of the 2006 ACM symposium on Applied computing, SAC '06, pp.1318-1322, 2006.

H. Luiz, J. De-figueiredo, and . Stolfi, Self-Validated Numerical Methods and Applications, Brazilian Mathematics Colloquium monographs. IMPA/CNPq, 1997.

D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal et al., Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software, Proceedings of Formal Methods in Industrial Critical Systems, pp.53-69, 2009.
DOI : 10.1007/978-3-642-04570-7_6

E. W. Cheney, Introduction to approximation theory, 1966.

]. B. Fla88 and . Flavigny, A new machine providing accuracy estimates of computation results [Flu] Fluctuat. Static analysis for numerical precision, 12th IMACS Congress, 1988.

J. Fillitre, C. March, and T. Hubert, The caduceus tool for the verification of c programs

. Gap and . Gappa, Gnration automatique de preuves de proprits arithmtiques

E. [. Ghorbal, S. Goubault, and . Putot, The Zonotope Abstract Domain Taylor1+, Proc. of the 21th Int. Conf. on Computer Aided Verification, pp.627-633, 2009.
DOI : 10.1007/978-3-642-02658-4_47

E. [. Ghorbal, S. Goubault, and . Putot, A Logical Product Approach to Zonotope Intersection, Proc. of the 22th Int. Conf. on Computer Aided Verification, 2010.
DOI : 10.1007/978-3-642-14295-6_22
URL : http://arxiv.org/abs/1002.2236

A. Girard, Reachability of Uncertain Linear Systems Using Zonotopes, Hybrid Systems: Computation and Control, pp.291-305, 2005.
DOI : 10.1007/978-3-540-31954-2_19
URL : https://hal.archives-ouvertes.fr/hal-00307003

A. Girard and C. L. Guernic, Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis, Hybrid Systems: Computation and Control, pp.215-228, 2008.
DOI : 10.1007/978-3-540-78929-1_16
URL : https://hal.archives-ouvertes.fr/hal-00306993

[. Goubault, M. Martel, and S. Putot, Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter, Proceedings of the 11th European Symposium on Programming Languages and Systems, ESOP '02, pp.209-212, 2002.
DOI : 10.1007/3-540-45927-8_15

M. [. Goubault, S. Martel, and . Putot, Some future challenges in the validation of control systems, European Congress on Embedded Real Time Software (ERTS), 2006.

L. J. Guibas, A. Nguyen, and L. Zhang, Zonotopes as bounding volumes, Proceedings of the fourteenth annual ACM-SIAM symposium on Discrete algorithms, SODA '03, pp.803-812, 2003.

]. D. Gol91 and . Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, 1991.

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

E. Goubault, Static Analyses of the Precision of Floating-Point Operations, Static Analysis, pp.234-259
DOI : 10.1007/3-540-47764-0_14

E. Goubault and S. Putot, Static Analysis of Numerical Algorithms, SAS, pp.18-34, 2006.
DOI : 10.1007/11823230_3

E. Goubault and S. Putot, Perturbed affine arithmetic for invariant computation in numerical program analysis. CoRR, abs/0807, p.2961, 2008.

E. Goubault and S. Putot, A zonotopic framework for functional abstractions. CoRR, abs/0910, 1763.

E. Goubault and S. Putot, Static Analysis of Finite Precision Computations, Verification, Model Checking, and Abstract Interpretation, pp.232-247, 2011.
DOI : 10.1007/978-3-540-24738-8_18

S. [. Goubault, P. Putot, J. Baufreton, and . Gassino, Static Analysis of the Accuracy in Control Systems: Principles and Experiments, Proceedings of Formal Methods in Industrial Critical Systems, 2007.
DOI : 10.1007/978-3-540-79707-4_3

[. Gulwani and A. Tiwari, Combining abstract interpreters, PLDI, pp.376-386, 2006.
DOI : 10.1145/1133255.1134026

]. E. Han69 and . Hansen, The centered form. Topics in Interval Analysis, pp.102-106, 1969.

E. R. Hansen, A generalized interval arithmetic, In Interval Mathematics, LNCS Commun. ACM, vol.29, issue.26, pp.7-1853, 1975.
DOI : 10.1007/3-540-07170-9_2

[. Std, 754 TM -2008 Standard for Floating-Point Arithmtic, pp.10016-5997, 2008.

J. Chesneaux, Cadna: a library for estimating round-off error propagation, Computer Physics Communications, vol.178, issue.12, pp.933-955, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01146486

D. [. Jansson, C. Chaykin, and . Keil, Rigorous Error Bounds for the Optimal Value in Semidefinite Programming, SIAM Journal on Numerical Analysis, vol.46, issue.1, pp.180-200, 2007.
DOI : 10.1137/050622870

[. Jean, Estimation de la prcision des rsultats de logiciels numriques, 1990.

J. Chesneaux, Modelisation et conditions de validit de la mthode cestac, 1988.

J. Faye, Implementation synchrone de cestac, 1989.

[. Kagiwada, Numerical derivatives and nonlinear analysis, 1986.
DOI : 10.1007/978-1-4684-5056-9

M. Karr, Affine relationships among variables of a program, Acta Informatica, vol.6, issue.2, pp.133-151, 1976.
DOI : 10.1007/BF00268497

[. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica, vol.244, issue.S, pp.373-396, 1984.
DOI : 10.1007/BF02579150

]. C. Kei05 and . Keil, Lurupa -rigorous error bounds in linear programming, Algebraic and Numerical Algorithms and Computer-assisted Proofs, 2005.

]. C. Kei08 and . Keil, A comparison of software packages for verified linear programming, 2008.

[. Kolev, Use of interval slopes for the irrational part of factorable functions, Reliable Computing, vol.3, issue.1, pp.83-93, 1997.
DOI : 10.1023/A:1009902813842

V. Lubomir and . Kolev, Automatic computation of a linear interval enclosure, Reliable Computing, vol.7, pp.17-28, 2001.

V. Lubomir and . Kolev, An improved interval linearization for solving nonlinear problems, Numerical Algorithms, vol.37, pp.213-224, 2004.

V. Lubomir and . Kolev, Optimal multiplication of g-intervals, Reliable Computing, vol.13, issue.5, pp.399-408, 2007.

[. Kühn, Zonotope Dynamics in Numerical Quality Control, Visualization and Mathematics, pp.125-134, 1998.
DOI : 10.1007/978-3-662-03567-2_10

V. Harvey-le, A note on Chernikova's algorithm, 1992.

[. Guernic, Reachability analysis of hybrid systems with linear continuous dynamics, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00422569

F. Vincent-laviron and . Logozzo, Subpolyhedra: A (more) scalable approach to infer linear inequalities, VM- CAI, pp.229-244, 2009.

M. Martel, Propagation of Roundoff Errors in Finite Precision Computations: A Semantics Approach, Proceedings of the 11th European Symposium on Programming Languages and Systems, ESOP '02, pp.194-208, 2002.
DOI : 10.1007/3-540-45927-8_14

F. Messine, Extensions of affine arithmetic: Application to unconstrained global optimization, Journal of Universal Computer Science, vol.8, pp.992-1015, 2002.

]. A. Min04a and . Miné, Relational abstract domains for the detection of floating-point run-time errors, Proc. of the European Symposium on Programming, pp.3-17, 2004.

]. A. Min04b and . Miné, Weakly Relational Numerical Abstract Domains, 2004.

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

]. A. Min06b and . Miné, Symbolic methods to enhance the precision of numerical abstract domains, VMCAI'06, pp.348-363, 2006.

[. Miyajima, On the improvement of the division of the affine arithmetic, 2000.

[. Miyajima and M. Kashiwagi, A dividing method utilizing the best multiplication in affine arithmetic, IEICE Electronics Express, vol.1, issue.7, pp.176-181, 2004.
DOI : 10.1587/elex.1.176

[. Miyajima and M. Kashiwagi, A Method Which Finds the Maxima and Minima of a Multivariable Function Applying Affine Arithmetic, NAA, pp.424-431, 2004.
DOI : 10.1007/978-3-540-31852-1_51

E. Ramon, C. T. Moore, and . Yang, Interval analysis I Lockheed Missiles and Space Division, 1959.

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.2828

. Pro and . Project, The Parma Polyhedra Library

K. [. Revol, M. Makino, and . Berz, Taylor models and floatingpoint arithmetic: proof that arithmetic operations are validated in cosy. The journal of Logic and Algebraic Programming, pp.135-154, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00071850

]. R. Roc70 and . Tyrrell-rockafellar, Convex Analysis, 1970.

J. Souyris and D. Delmas, Experimental Assessment of Astr??e on Safety-Critical Avionics Software, Computer Safety, Reliability, and Security, pp.479-490, 2007.
DOI : 10.1007/978-3-540-75101-4_45

A. Simon, A. King, and J. M. Howe, Two Variables per Linear Inequality as an Abstract Domain, Proceedings of the 12th international conference on Logic based program synthesis and transformation, LOPSTR'02, pp.71-89, 2003.
DOI : 10.1007/3-540-45013-0_7

[. Shou, H. Lin, R. R. Martin, and G. Wang, Modified affine arithmetic in tensor form for trivariate polynomial evaluation and algebraic surface plotting, Journal of Computational and Applied Mathematics, vol.195, issue.1-2, pp.155-171, 2006.
DOI : 10.1016/j.cam.2005.08.003

J. Michael, J. E. Schulte, and . Stine, A combined interval and floating-point divider. Signals, Systems and Computers, pp.218-222, 1998.

D. Speyer and B. Sturmfels, Tropical Mathematics, Mathematics Magazine, vol.82, issue.3, 2004.
DOI : 10.4169/193009809X468760

[. Sankaranarayanan, H. B. Sipma, and Z. Manna, Scalable Analysis of Linear Systems Using Mathematical Programming, VMCAI, pp.25-41, 2005.
DOI : 10.1007/978-3-540-30579-8_2

H. Pat and . Sterbenz, Floating-point Computation. Prentice-Hall series in automatic computation, 1974.

]. A. Tar55 and . Tarsky, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math, vol.5, pp.285-309, 1955.

]. J. Vig78 and . Vignes, New methods for evaluating the validity of the results of mathematical computations, Mathematics and Computers in Simulation, vol.20, issue.4, pp.227-249, 1978.

]. J. Vig93 and . Vignes, A stochastic arithmetic for reliable scientific computation, Mathematics and Computers in Simulation, vol.35, issue.3, pp.233-261, 1993.

S. Zuhe and M. A. Wolfe, On interval enclosures using slope arithmetic, Applied Mathematics and Computation, vol.39, issue.1, pp.89-105, 1990.
DOI : 10.1016/0096-3003(90)90124-L