P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice, LUSTRE: a declarative language for real-time programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '87, pp.178-188, 1987.
DOI : 10.1145/41625.41641

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 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

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

S. Gaubert, E. Goubault, A. Taly, and S. Zennou, Static Analysis by Policy Iteration on Relational Domains, European Symposium on Programming, pp.237-252, 2007.
DOI : 10.1007/978-3-540-71316-6_17

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

T. Gawlitza and H. Seidl, Precise Fixpoint Computation Through Strategy Iteration, European Symposium on Programming, pp.300-315, 2007.
DOI : 10.1007/978-3-540-71316-6_21

T. Gawlitza and H. Seidl, Precise Relational Invariants Through Strategy Iteration, In: Computer Science Logic. LNCS, vol.4646, pp.23-40, 2007.
DOI : 10.1007/978-3-540-74915-8_6

T. Gawlitza, H. Seidl, A. Adjé, S. Gaubert, and E. Goubault, Abstract interpretation meets convex optimization, Journal of Symbolic Computation, vol.47, issue.12, pp.1416-1446, 2012.
DOI : 10.1016/j.jsc.2011.12.048

URL : https://hal.archives-ouvertes.fr/hal-00778070

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

P. Cousot and R. Cousot, Static determination of dynamic properties of programs, Proceedings of the Second International Symposium on Programming, pp.106-130, 1976.

A. Miné, A New Numerical Abstract Domain Based on Difference-Bound Matrices, LNCS, vol.2053, pp.155-172, 2001.
DOI : 10.1007/3-540-44978-7_10

A. Miné, The octagon abstract domain, Working Conference on Reverse Engineering IEEE, pp.310-319, 2001.

T. Bultan, R. Gerber, and W. Pugh, Symbolic model checking of infinite state systems using presburger arithmetic, LNCS, vol.1254, pp.400-411, 1997.
DOI : 10.1007/3-540-63166-6_39

B. Jeannet, N. Halbwachs, and P. Raymond, Dynamic Partitioning in Analyses of Numerical Properties, Static Analysis Symposium, pp.39-50, 1999.
DOI : 10.1007/3-540-48294-6_3

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

G. Hagen and C. Tinelli, Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques, 2008 Formal Methods in Computer-Aided Design, pp.1-9, 2008.
DOI : 10.1109/FMCAD.2008.ECP.19

T. Gawlitza and H. Seidl, Precise Interval Analysis vs. Parity Games, LNCS, vol.5014, pp.342-357, 2008.
DOI : 10.1007/978-3-540-68237-0_24

T. M. Gawlitza and H. Seidl, Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely, Static Analysis Symposium, pp.271-286, 2010.
DOI : 10.1007/978-3-642-15769-1_17

T. M. Gawlitza and H. Seidl, Solving systems of rational equations through strategy iteration, ACM Transactions on Programming Languages and Systems, vol.33, issue.3, p.11, 2011.
DOI : 10.1145/1961204.1961207

B. Jeannet, BDDAPRON: A logico-numerical abstract domain library, 2009.

P. Sotin, B. Jeannet, F. Védrine, and E. Goubault, Policy iteration within logiconumerical abstract domains In: Automated Technology for Verification and Analysis, LNCS, vol.6996, pp.290-305, 2011.

L. Gonnord and N. Halbwachs, Combining Widening and Acceleration in Linear Relation Analysis, Static Analysis Symposium, pp.144-160, 2006.
DOI : 10.1007/11823230_10

URL : https://hal.archives-ouvertes.fr/hal-00189614

P. Schrammel and B. Jeannet, Applying abstract acceleration to (co-)reachability analysis of reactive programs, Journal of Symbolic Computation, vol.47, issue.12, pp.1512-1532, 2012.
DOI : 10.1016/j.jsc.2011.12.051

URL : https://hal.archives-ouvertes.fr/hal-00753412

P. Schrammel and B. Jeannet, Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs, Static Analysis Symposium, pp.233-248, 2011.
DOI : 10.1007/s10703-006-0031-0

URL : https://hal.archives-ouvertes.fr/inria-00596241

D. Gopan and T. W. Reps, Guided Static Analysis, Static Analysis Symposium, pp.349-365, 2007.
DOI : 10.1007/978-3-540-74061-2_22

T. Dang and T. M. Gawlitza, Discretizing Affine Hybrid Automata with Uncertainty, LNCS, pp.473-481, 2011.
DOI : 10.1007/978-3-642-24372-1_36

B. Jeannet and A. Miné, Apron: A Library of Numerical Abstract Domains for Static Analysis, LNCS, vol.5643, pp.661-667, 2009.
DOI : 10.1007/978-3-642-02658-4_52

URL : https://hal.archives-ouvertes.fr/hal-00786354

P. Schrammel and B. Jeannet, From hybrid data-flow languages to hybrid automata, Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, HSCC '12, pp.167-176, 2012.
DOI : 10.1145/2185632.2185658

URL : https://hal.archives-ouvertes.fr/hal-00659698

T. Dang and T. M. Gawlitza, Template-based unbouded time verification of affine hybrid automata, Asian Symposium on Programming Languages and Systems, pp.34-49, 2011.