R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. H. Ho et al., The algorithmic analysis of hybrid systems, Hybrid Systems I, volume 736 of Lecture Notes in Computer Science, pp.3-34, 1992.
DOI : 10.1016/0304-3975(94)00202-T

R. Alur, D. L. Dillagg08-]-x.-allamigeon, S. Gaubert, and E. Goubault, A theory of timed automata, Proceedings of the 15th International Static Analysis Symposium (SAS'08 Special issue on hybrid systems : theory and applications of Proceedings of the IEEEBCC + 03, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation (PLDI'03), pp.196-207, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00128135

J. Bertrane, Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs, Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation Hoffstätter. Computation and application of taylor polynomials with interval remainder bounds. Reliable Computing, pp.97-11283, 1998.
DOI : 10.1007/978-3-540-30579-8_7

C. Bischof, P. Hovland, and B. Norris, Implementation of automatic differentiation tools. SIGPLAN Notices, Bie51] L. Bieberbach. On the remainder of the Runge-Kutta formula. Zeitschrift für angewandte Mathematik und Physik, pp.98-107233, 1951.

G. Birkhoff, Lattice Theory Amer, 1967.

I. Bogudlov, T. Lev-ami, T. Reps, and M. Sagiv, Revamping TVLA: Making Parametric Shape Analysis Competitive, 19th International Conference on Computer Aided Verification (CAV'07), pp.221-225, 2007.
DOI : 10.1007/978-3-540-73368-3_25

M. Berz and K. Makino, Verified integration of odes and flows using differential algebraic methods on high-order taylor models, Reliable Computing, vol.4, issue.4, pp.361-369, 1998.
DOI : 10.1023/A:1024467732637

]. M. Bm06a, K. Berz, and . Makino, COSY INFINITY Version 9, Nuclear Instruments and Methods, vol.558, pp.346-350, 2006.

]. O. Bm06b, M. Bouissou, and . Martel, GRKLib : a guaranteed runge-kutta library, International Symposium on Scientific Computing, 2006.

O. Bouissou and M. Martel, GRKLib: a Guaranteed Runge Kutta Library, 12th GAMM, IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2006), 2007.
DOI : 10.1109/SCAN.2006.20

O. Bouissou and M. Martel, Static analysis of embedded programs with continuous i/o (poster), Hybrid Systems, Computation and Control (HSCC'07), 2007.

O. Bouissou and M. Martel, Abstract Interpretation of the Physical Inputs of Embedded Programs, Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'08), pp.37-51, 2008.
DOI : 10.1007/978-3-540-78163-9_8

]. O. Bm08b, M. Bouissou, and . Martel, A hybrid denotational semantics of hybrid systems, Proceedings of the 17th European Symposium on Programming Languages and Systems, pp.63-77, 2008.

[. Budde, A. Poigné, and K. Sylla, synERJY An Object-oriented Synchronous Language, Electronic Notes in Theoretical Computer Science, vol.153, issue.4, pp.99-115, 2006.
DOI : 10.1016/j.entcs.2006.02.026

R. Bagnara, E. Ricci, E. Zaffanella, and P. Hill, Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library, Proceedings of the 9th International Symposium on Static Analysis (SAS'02), pp.213-229, 2002.
DOI : 10.1007/3-540-45789-5_17

C. Bendtsen and O. Stauning, FADBAD, a flexible c++ package for automatic differentiation using the forward and backward methods, 1996.

W. [. Baeten and . Weijland, Process algebra, 1990.

P. [. Bachmann, E. Wang, and . Zima, Chains of recurrences---a method to expedite the evaluation of closed-form functions, Proceedings of the international symposium on Symbolic and algebraic computation , ISSAC '94, pp.242-249, 1994.
DOI : 10.1145/190347.190423

]. J. Car58 and . Carr, Error bounds for the Runge-Kutta single-step integration process, Journal of the ACM, vol.5, issue.1, pp.39-44, 1958.

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. Cc92a, R. Cousot, and . Cousot, Abstract interpretation frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.

]. P. Cc92b, R. Cousot, . [. Cousot, R. Cousot, and . Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper, Proceedings of the 4th International Workshop Programming Language Implementation and Logic Programming (PLILP'92) Proceedings of the 1994 International Conference on Computer Languages, pp.269-295, 1992.

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, R. Cousot, J. Feret, L. Mauborgne, A. Minéand et al., The ASTRE?? Analyzer, Proceedings of the 14th European Symposium on Programming (ESOP'05), pp.21-30, 2005.
DOI : 10.1007/978-3-540-31987-0_3

Y. Chen, E. Gansner, E. Koutsofios, . C++-b, A. Cook et al., A C++ data model supporting reachability analysis and dead code detection, Proceedings of the 6th European Software Engineering Conference Conference Record of the Fifth ACM Symposium on Principles of Programming Languages (POPL'78) Proceedings of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05) Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation (PLDI'06)CPR06b] B. Cook, A. Podelski, and A. Rybalchenko. Terminator : Beyond safety 18th International Conference on Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer ScienceDHL + 05, pp.414-431265, 1973.
DOI : 10.1007/3-540-63531-9_28

D. Daney, G. Hanrot, V. Lefèvre, P. Pélissier, F. Rouillier et al., The MPFR library Astrée : From research to industry [Eij81] P. Eijgenraam. The Solution of Initial Value Problems Using Interval Arithmetic, Proceedings of the 14th International Symposium on Static Analysis (SAS'07), pp.437-451, 1981.

A. Edalat and A. Lieutier, Domain theory and differential calculus (functions of one variable), Mathematical Structures in Computer Science, vol.14, issue.6, pp.771-802, 2002.
DOI : 10.1017/S0960129504004359

A. Edalat and D. Pattinson, A Domain Theoretic Account of Picard???s Theorem, 31st International Colloquium on Automata, Languages and Programming, pp.494-505, 2004.
DOI : 10.1007/978-3-540-27836-8_43

J. Feret, Static Analysis of Digital Filters, Proceedings of the 13th European Symposium on Programming Languages and Systems, pp.33-48, 2004.
DOI : 10.1007/978-3-540-24725-8_4
URL : https://hal.archives-ouvertes.fr/inria-00528447

]. J. Fer05 and . Feret, The arithmetic-geometric progression abstract domain, Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), pp.42-58, 2005.

C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt et al., Reliable and Precise WCET Determination for a Real-Life Processor, First International Workshop on Embedded Software (EMSOFT'01), volume 2211 of Lecture Notes in Computer Science, pp.469-485, 2001.
DOI : 10.1007/3-540-45449-7_32

K. Forsberg and H. Mooz, The Relationship of Systems Engineering to the Project Cycle, Engineering Management Journal, vol.4, issue.3, pp.36-38, 1992.
DOI : 10.1080/10429247.1992.11414684

]. G. Fre05 and . Frehse, Phaver : Algorithmic verification of hybrid systems past hytech, Proceedings of the , 8th International Workshop on Hybrid Systems : Computation and Control (HSCC'05), pp.258-273, 2005.

[. Gao, Patriot missile defense : Software problem led to system failure at Dhahran, Saudi Arabia, U.S. General Accouting Office, 1992.

[. Guernic and A. Girard, Zonotope-hyperplane intersection for hybrid systems reachability analysis, Proceedings of the International Workshop on Hybrid Systems : Computation and Control, pp.215-228, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00306993

. Ghk-+-03-]-g, K. H. Gierz, K. Hofmann, J. D. Keimel, M. Lawson et al., Continuous Lattices and Domains, 2003.

R. [. Gupta, V. Jagadeesan, and . Saraswat, Computing with continuous change, Science of Computer Programming, vol.30, issue.1-2, pp.3-49, 1998.
DOI : 10.1016/S0167-6423(97)00006-3
URL : http://doi.org/10.1016/s0167-6423(97)00006-3

R. [. Gupta, V. Jagadeesan, D. Saraswat, and . Bobrow, Programming in hybrid constraint languages, Hybrid Systems II, 1995.
DOI : 10.1007/3-540-60472-3_12

E. 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), volume 2305 of Lecture Notes in Computer Science, pp.209-212, 2002.
DOI : 10.1007/3-540-45927-8_15

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

]. E. Gou01 and . Goubault, Static analyses of floating-point operations, Proceedings of the 8th International Static Analysis Symposium (SAS'01), pp.234-259, 2001.

E. Goubault and S. Putot, Static Analysis of Numerical Algorithms, Proceedings of the 13th International Symposium on Static Analysis (SAS'06), pp.18-34, 2006.
DOI : 10.1007/11823230_3

]. P. Gra91, ]. Grangergri00, and . Griewank, Static analysis of linear congruence equalities among variables of a program theory and practice of software development on Colloquium on trees in algebra and programming (TAPSOFT'91) Evaluating derivatives : principles and techniques of algorithmic differentiation, International joint conference on, pp.169-192, 1991.

V. Gupta, V. Saraswat, and P. Struss, A model of a photocopier paper path, Workshop on Engineering Problems for Qualitative Reasoning, 1995.

]. K. Gus91 and . Gustafsson, Control theoretic techniques for stepsize selection in explicit rungekutta methods Control of error and convergence in ODE solvers, ACM Transaction on Mathematical Software, vol.17, issue.4, pp.533-554, 1991.

B. [. Heemels, A. Schutter, and . Bemporad, Equivalence of hybrid dynamical models, Automatica, vol.37, issue.7, pp.1085-1091, 2001.
DOI : 10.1016/S0005-1098(01)00059-0

]. T. Hen96 and . Henzinger, The theory of hybrid automata, Symposium on Logic in Computer Science, pp.278-292, 1996.

J. Hespanha, Uniform Stability of Switched Linear Systems: Extensions of LaSalle's Invariance Principle, IEEE Transactions on Automatic Control, vol.49, issue.4, pp.470-482, 2004.
DOI : 10.1109/TAC.2004.825641

R. Heckmann and C. Ferdinand, Verifying Safety-Critical Timing and Memory-Usage Properties of Embedded Software by Abstract Interpretation, Design, Automation and Test in Europe, pp.618-619, 2005.
DOI : 10.1109/DATE.2005.326
URL : https://hal.archives-ouvertes.fr/hal-00181577

P. [. Henzinger and . Ho, A note on abstract interpretation strategies for hybrid automata, Hybrid Systems II, pp.252-264, 1995.
DOI : 10.1007/3-540-60472-3_13

B. [. Henzinger, R. Horowitz, H. Majumdar, and . Wong-toi, Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods, Third International Workshop on Hybrid Systems : Computation and Control, pp.130-144, 2000.
DOI : 10.1007/3-540-46430-1_14

P. [. Henzinger, H. Ho, and . Wong-toi, HyTech: A model checker for hybrid systems, Proceedings of the 9th International Conference Computer Aided Verification, pp.460-463, 1997.
DOI : 10.1007/3-540-63166-6_48

P. [. Henzinger, H. Ho, and . Wong-toi, Algorithmic analysis of nonlinear hybrid systems, ACM Symposium on Theory of computing, pp.540-554, 1995.
DOI : 10.1109/9.664156

O. [. Hymans, . Levillain, I. Newspeak, S. M. Heymann, F. Lin et al., Doubleplussimple Minilang for Goodthinkful Static Analysis of C. Technical Note 2008-IW-SE-00010-1 Analysis of zeno behaviors in hybrid systems Symbolic model checking for rectangular hybrid systems, Proceedings of the Sixth International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pp.376-384, 2000.

]. C. Hoa78 and . Hoare, Communicating sequential processes, Commun. ACM, vol.21, issue.8, pp.666-677, 1978.

]. C. Hoa85, . Hoarehpr94-]-n, Y. Halbwachs, P. Proy, and . Raymond, Communicating Sequential Processes Verification of linear hybrid systems by means of convex approximations, First International Static Analysis Symposium (SAS'94), pp.223-237, 1985.

V. [. Henzinger and . Rusu, Reachability verification for hybrid automata, First InternationalWorkshop on Hybrid Systems : Computation and Control (HSCC'98), pp.190-204, 1998.
DOI : 10.1007/3-540-64358-3_40
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.773

]. E. Inc56 and . Ince, Ordinary Differential Equations, 1956.

K. H. Johansson, M. Egerstedt, J. Lygeros, and S. Sastry, On the regularization of zeno hybrid automata. Systems and control letters, pp.141-150, 1999.

L. Jaulin, M. Kieffer, O. Didrit, and E. Walter, Applied Interval Analysis, 2001.
DOI : 10.1007/978-1-4471-0249-6
URL : https://hal.archives-ouvertes.fr/hal-00845131

K. Johansson, J. Lygeros, S. S. Sastry, M. Egerstedtjoh77, and ]. S. Johnson, Simulation of zeno hybrid automata Lint, a C program checker, IEEE Conference on Decision and ControlKnu94] O. Knuppel. PROFIL/BIAS : a fast interval library. Computing, pp.3538-35433, 1977.

D. Kozen, Results on the propositional ??-calculus, Theoretical Computer Science, vol.27, issue.3, pp.333-354, 1983.
DOI : 10.1016/0304-3975(82)90125-6

]. S. Ksf-+-99, O. Kowalewski, M. Stursberg, H. Fritz, I. H. Graf et al., A case study in tool-aided analysis of discretely controlled continuous systems : the two tanks problem, Hybrid Systems V, volume 1567 of Lecture Notes in Computer Science, 1999.

]. J. Ljs-+-03, K. H. Lygeros, S. N. Johansson, J. Simic, S. S. Zhang et al., Dynamical properties of hybrid automata, IEEE Transactions on Automatic Control, vol.48, issue.1, pp.2-17, 2003.

]. E. Lor63 and . Lorenz, Deterministic nonperiodic flow, Journal of the Atmospheric Sciences, vol.20, issue.2, pp.130-141, 1963.

Y. Lin, M. A. Stadtherr, N. Lynch, R. Segala, F. Vaandrager et al., Validated solutions of initial value problems for parametric ODEs, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control, pp.1145-1162, 1996.
DOI : 10.1016/j.apnum.2006.10.006

]. R. Lö88 and . Löhner, Einschließung der Lösung gewöhnlicher Anfangsund Randwertaufgaben und Anwendungen, 1988.

]. R. Lö95 and . Löhner, Step size and order control in the verified solution of IVP with ODE's, International conference on scientific computation and differential equations (SciSCADE'95), 1995.

]. M. Mar02 and . 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), volume 2305 of Lecture Notes in Computer Science, pp.194-208, 2002.

M. Martel, An Overview of Semantics for the Validation of Numerical Programs, Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), pp.59-77, 2005.
DOI : 10.1007/978-3-540-30579-8_4

M. Martel, Semantics of roundoff error propagation in finite precision calculations, Higher Order Symbolic Computation, pp.7-30, 2006.
DOI : 10.1007/s10990-006-8608-2

]. D. Mas02 and . Massé, Temporal Property-driven Verification by Abstract Interpretation, 2002.

J. Meinadier, Ingénierie et intégration des systèmes. Collection Etudes et logiciels informatiques, 1998.

]. P. Mel94 and . Mellor, CAD : Computer aided disaster, SOFSEM, pp.147-180, 1994.

R. Milner, Communicating and Mobile Systems : the Pi-Calculus, 1999.

J. S. Miller, Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata, Third International Workshop on Hybrid Systems : Computation and Control, pp.296-309, 2000.
DOI : 10.1007/3-540-46430-1_26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.455.2409

]. A. Min01 and . Miné, The octagon abstract domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), IEEE, pp.310-319, 2001.

[. Makhlouf and S. Kowalewski, An evaluation of two recent reachability analysis tools for hybrid systems, Second IFAC Conference on Analysis and Design of Hybrid Systems, pp.377-382, 2006.

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

]. R. Moo79 and . Moore, Methods and Applications of Interval Analysis, SIAM, 1979.

]. N. Ned06 and . Nedialkov, Interval tools for ODEs and DAEs, 2006.

[. Nita, D. Grossman, C. S. Chambersnj99-]-n, K. R. Nedialkov, and . Jackson, A theory of platform-dependent lowlevel software An interval Hermite-Obreschkoff method for computing rigorous bounds on the solution of an initial value problem for an ordinary differential equation, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Developments in Reliable Computing, pp.209-220, 1999.

]. N. Nj01a, K. R. Nedialkov, and . Jackson, The design and implementation of an objectoriented validated ODE solver, 2001.

]. N. Nj01b, K. R. Nedialkov, and . Jackson, A new perspective on the wrapping effect in interval methods for initial value problems for ordinary differential equations, Perspectives on Enclosure Methods, pp.219-264, 2001.

K. [. Nedialkov, G. F. Jackson, and . Corliss, Validated solutions of initial value problems for ordinary differential equations, Applied Mathematics and Computation, vol.105, issue.1, pp.21-68, 1999.
DOI : 10.1016/S0096-3003(98)10083-8

K. [. Nedialkov, J. D. Jackson, and . Pryce, An effective high-order interval method for validating existence and uniqueness of the solution of an IVP for an ODE, Reliable Computing, vol.7, issue.6, pp.449-465, 2001.
DOI : 10.1023/A:1014798618404

H. [. Otter, S. E. Elmqvist, and . Mattsson, Hybrid modeling in Modelica based on the synchronous data flow principle, Proceedings of the 1999 IEEE International Symposium on Computer Aided Control System Design (Cat. No.99TH8404), pp.151-157, 1999.
DOI : 10.1109/CACSD.1999.808640

[. Task and P. Ansi, Standard for Binary Floating-Point Arithmetic, pp.754-1985, 1985.

A. Platzer and E. Clarke, The Image Computation Problem in Hybrid Systems Model Checking, 10th International Workshop on Hybrid Systems : Computation and Control, pp.473-486, 2007.
DOI : 10.1007/978-3-540-71493-4_37

E. [. Putot, M. Goubault, and . Martel, Static Analysis-Based Validation of Floating-Point Computations, Numerical Software with Result Verification, pp.306-313, 2003.
DOI : 10.1007/978-3-540-24738-8_18

]. S. Pop06 and . Pop, The SSA Representation Framework : Semantics, Analyses and GCC Implementation, 2006.

K. [. Revol, M. Makino, and . Berz, Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY, The Journal of Logic and Algebraic Programming, vol.64, issue.1, pp.135-154, 2005.
DOI : 10.1016/j.jlap.2004.07.008
URL : https://hal.archives-ouvertes.fr/inria-00071850

W. C. Rounds and H. Song, The phi-calculus -a hybrid extension of the pi-calculus to embedded systems, 2002.

W. C. Rounds and H. Song, The ??-Calculus: A Language for Distributed Control of Reconfigurable Embedded Systems, 6th International Workshop on Hybrid Systems : Computation and Control (HSCC'03), pp.435-449, 2003.
DOI : 10.1007/3-540-36580-X_32

J. Stoer, R. F. Bulirschsha05-]-l, and . Shampine, Introduction to Numerical Analysis Error estimation and control for odes, Journal of Scientific Computing, vol.25, issue.12, pp.3-16, 1993.

M. [. Saraswat, P. Rinard, and . Panangaden, The semantic foundations of concurrent constraint programming, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.333-352, 1991.
DOI : 10.1145/99583.99627

J. [. Van-der-schaft and . Schumacher, An Introduction to Hybrid Dynamical Systems, Lecture Notes in Control and Information Sciences, vol.251, 2000.
DOI : 10.1007/BFb0109998

O. Stauning, Automatic Validation of Numerical Solutions, 1997.

]. N. Sto96 and . Storey, Safety Critical Computer Systems, 1996.

]. K. Str99 and . Strehl, Interval diagrams : Increasing efficiency of symbolic real-time verification [Tar55] A. Tarski. A lattice-theoretical fixpoint theorem and its applications, Proceedings of the Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), pp.488285-309, 1955.

A. Venet and G. Brat, Precise and efficient static array bound checking for large embedded C programs, ACM SIGPLAN Notices, vol.39, issue.6, pp.231-242, 2004.
DOI : 10.1145/996893.996869

]. D. Van-beek, K. Man, M. Reniers, J. Rooda, and R. Schiffelers, Syntax and consistent equation semantics of hybrid Chi, The Journal of Logic and Algebraic Programming, vol.68, issue.1-2, pp.129-210, 2006.
DOI : 10.1016/j.jlap.2005.10.005

J. Zhang, K. Johansson, J. Lygeros, and S. Sastry, Zeno hybrid systems, International Journal of Robust and Nonlinear Control, vol.35, issue.5, pp.435-451, 2001.
DOI : 10.1002/rnc.592