=. Acbc, *. Qmu, E. <=, and . Ep, inv() * AcBc.T).inv() 35 ER = Ellipsoid(R) 36 print("ER included in EP

=. Erbar, ERbar included in EP :", ER <= EP) Listing 4.1: Computation of E R using LyaFloat Bibliography, ACD93] R. Alur, C. Courcoubetis, and D. Dill. Model-Checking in Dense Real-Time. Information and Computation, pp.43-45, 1993.

F. [. Ancourt, F. Coelho, and . Irigoin, A Modular Static Analysis Approach to Affine Loop Invariants Detection, Electronic Notes in Theoretical Computer Science, vol.267, issue.1, pp.3-16, 2010.
DOI : 10.1016/j.entcs.2010.09.002
URL : https://hal.archives-ouvertes.fr/hal-00586338

C. Ancourt, F. Coelho, F. Irigoin, and R. Keryell, A Linear Algebra Framework for Static HPF Code Distribution, Scientific Programming, pp.3-27, 1997.
URL : https://hal.archives-ouvertes.fr/hal-00752595

D. [. Alur and . Dill, Automata for modeling real-time systems, Automata , Languages and Programming, pp.322-335, 1990.
DOI : 10.1007/BFb0032042

C. Alias, A. Darte, P. Feautrier, and L. Gonnord, Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs, Static Analysis, pp.117-133, 2010.
DOI : 10.1007/978-3-642-15769-1_8
URL : https://hal.archives-ouvertes.fr/inria-00523298

]. Z. Amm92 and . Ammarguellat, A Control-Flow Normalization Algorithm and its Complexity, IEEE Transactions on Software Engineering, vol.18, issue.3, pp.237-251, 1992.

F. [. Alpern and . Schneider, Recognizing safety and liveness, Distributed Computing, pp.117-12610, 1987.
DOI : 10.1007/BF01782772

]. D. Avi98 and . Avis, Computational Experience with the Reverse Search Vertex Enumeration Algorithm. Optimization Methods and Software, pp.107-124, 1998.

]. S. Bar05 and . Bardin, Vers un model checking avec accélération plate des systèmes hétérogènes, 2005.

. S. Bbc-+-00-]-n, A. Bjørner, M. A. Browne, B. Colón, Z. Finkbeiner et al., Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods in System Design, pp.227-270101008700623084, 1023.

A. [. Bardin, J. Finkel, and . Leroux, FASTer Acceleration of Counter Automata in Practice, Tools and Algorithms for the Construction and Analysis of Systems, pp.576-590, 2004.
DOI : 10.1007/978-3-540-24730-2_42

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

R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella, Precise widening operators for convex polyhedra, Science of Computer Programming, vol.58, issue.1-2, pp.28-56, 2005.
DOI : 10.1016/j.scico.2005.02.003

K. [. Bielecki, T. Kraska, and . Klimek, Transitive Closure of a Union of Dependence Relations for Parameterized Perfectly-Nested Loops, Parallel Computing Technologies, pp.37-50
DOI : 10.1007/978-3-642-39958-9_4

Y. [. Bensalem, S. Lakhnech, and . Owre, InVeSt : A Tool for the Verification of Invariants [bor95] Specification and Validation Methods, Computer Aided Verification, pp.505-510, 1995.

]. F. Bou92 and . Bourdoncle, Abstract Interpretation by Dynamic Partitioning, Journal of Functional Programming, vol.2, issue.04, pp.40710-1017, 1992.

G. Boudol, V. Roy, R. Simone, and D. Vergamini, Process calculi, from theory to practice: Verification tools, Automatic Verification Methods for Finite State Systems, pp.1-10, 1990.
DOI : 10.1007/3-540-52148-8_1
URL : https://hal.archives-ouvertes.fr/inria-00075461

]. J. Brz64 and . Brzozowski, Derivatives of Regular Expressions, Journal of the ACM, vol.11, issue.4, pp.481-494, 1964.

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

P. [. Boigelot and . Wolper, Symbolic verification with periodic sets, Computer Aided Verification, pp.55-67, 1994.
DOI : 10.1007/3-540-58179-0_43

]. P. Cc77a, R. Cousot, and . Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, pp.238-252, 1977.

]. P. Cc77b, R. Cousot, and . Cousot, Static Determination of Dynamic Properties of Generalized Type Unions, pp.77-94, 1977.

R. [. Cousot and . Cousot, Abstract interpretation and application to logic programs, The Journal of Logic Programming, vol.13, issue.2-3, pp.103-17910, 1992.
DOI : 10.1016/0743-1066(92)90030-7

J. [. Clarisó and . Cortadella, The octahedron abstract domain, Science of Computer Programming, vol.64, issue.1, pp.115-139, 2007.
DOI : 10.1016/j.scico.2006.03.009

. Ccf-+-15-]-p, R. Cousot, J. Cousot, A. Feret, and X. Miné, The Astrée Static Analyzer, 2001.

B. A. Chawdhary, S. Cook, M. Gulwani, H. Sagiv, and . Yang, Ranking Abstractions, Programming Languages and Systems, pp.148-162
DOI : 10.1007/978-3-540-78739-6_13

. Cen15, . Centre-de-recherche-en-informatique, and . Paristech, PIPS: Automatic Parallelizer and Code Transformation Framework, 1988.

E. [. Clarke, A. P. Emerson, and . Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-26310, 1986.
DOI : 10.1145/5397.5399

O. [. Clarke, D. E. Grumberg, and . Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1512-1542, 1994.
DOI : 10.1145/186025.186051

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

]. N. Che68 and . Chernikoba, Algorithm for Discovering the Set of All the Solutions of a Linear Programming Problem, USSR Computational Mathematics and Mathematical Physics, vol.8, issue.668, pp.282-29310, 1968.

Y. [. Comon and . Jurski, Multiple counters automata, safety analysis and presburger arithmetic, Computer Aided Verification, pp.268-279
DOI : 10.1007/BFb0028751

]. P. Cou05 and . Cousot, Proving Program Invariance and Termination by Parametric Abstraction , Lagrangian Relaxation and Semidefinite Programming, Verification, Model Checking, and Abstract Interpretation, pp.1-24, 2005.

A. [. Cook, A. Podelski, and . Rybalchenko, Termination Proofs for Systems Code

H. [. Colón and . Sipma, Synthesis of Linear Ranking Functions, Tools and Algorithms for the Construction and Analysis of Systems, pp.67-81, 2001.
DOI : 10.1007/3-540-45319-9_6

H. [. Colón and . Sipma, Practical Methods for Proving Program Termination, Computer Aided Verification, pp.442-454, 2002.
DOI : 10.1007/3-540-45657-0_36

]. Fer90 and . Fernandez, An Implementation of an Efficient Algorithm for Bisimulation Equivalence, Science of Computer Programming, vol.13, issue.2-390, pp.219-236, 1990.

]. E. Fer10 and . Feron, From Control Systems to Control Software, IEEE Control Systems Magazine, vol.30, issue.6, pp.50-71, 2010.

L. [. Feautrier and . Gonnord, Accelerated Invariant Generation for C Programs with Aspic and C2fsm, Electronic Notes in Theoretical Computer Science, vol.267, issue.2, pp.3-13, 2010.
DOI : 10.1016/j.entcs.2010.09.014
URL : https://hal.archives-ouvertes.fr/inria-00523320

]. R. Flo93 and . Floyd, Assigning Meanings to Programs, Program Verification, pp.65-81, 1993.

A. [. Fukuda and . Prodon, Double description method revisited, In Combinatorics and Computer Science Lecture Notes in Computer Science, vol.1120, pp.91-111, 1996.
DOI : 10.1007/3-540-61576-8_77
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8343

G. [. Finkel and . Sutre, An Algorithm Constructing the Semilinear Post for 2-Dim Reset/Transfer VASS, Mathematical Foundations of Computer Science, pp.353-362, 2000.
DOI : 10.1007/3-540-44612-5_31

. S. Ghk-+-06-]-b, T. A. Gulavani, Y. Henzinger, A. V. Kannan, S. K. Nori et al., SYNERGY: A New Algorithm for Property Checking. page 117, 2006.

S. [. Gulwani, E. Jain, and . Koskinen, Control-flow refinement and progress invariants for bound analysis, ACM SIGPLAN Notices, vol.44, issue.6, p.375, 2009.
DOI : 10.1145/1543135.1542518

C. [. Graf and . Loiseaux, A tool for symbolic program verification and abstraction, Computer Aided Verification, pp.71-84, 1993.
DOI : 10.1007/3-540-56922-7_7

K. [. Gulwani, T. Mehra, and . Chilimbi, SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. page 127, 2008.

]. D. Gol91 and . Goldberg, What Every Computer Scientist Should Know About Floating-Point Arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-48, 1991.

L. Gonnord, Accélération abstraite pour l'amélioration de la précision en analyse des relations linéaires, 2007.

]. L. Gon13 and . Gonnord, Aspic: Accelerated Symbolic Polyhedral Invariant Computation, pp.2010-2013

T. [. Gopan and . Reps, Lookahead Widening, Computer Aided Verification, pp.452-466, 2006.
DOI : 10.1007/11817963_41

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

]. P. Gra91 and . Granger, Analyses sémantiques de congruence, 1991.

]. S. Gul09 and . Gulwani, SPEED: Symbolic Complexity Bound Analysis, Computer Aided Verification, pp.51-62, 2009.

F. [. Gulwani and . Zuleger, The Reachability-Bound Problem. page 292, 2010.

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

]. N. Hal93 and . Halbwachs, Delay Analysis in Synchronous Programs, Computer Aided Verification, pp.333-346, 1993.

]. N. Hal10 and . Halbwachs, Linear Relation Analysis Principles and Recent Progress, 2010.

V. [. Haddad and . Chellaboina, Nonlinear Dynamical Systems and Control: A Lyapunov-Based Approach, 2011.

]. J. Hen11 and . Henry, Static Analysis by Abstract Interpretation, Path Focusing, 2011.

J. [. Halbwachs and . Henry, When the Decreasing Sequence Fails, Static Analysis, pp.198-213, 2012.
DOI : 10.1007/978-3-642-33125-1_15
URL : https://hal.archives-ouvertes.fr/hal-00734340

]. N. Hig02 and . Higham, Accuracy and Stability of Numerical Algorithms, 2002.

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Lazy Abstraction, pp.58-70, 2002.
DOI : 10.1145/565816.503279

F. [. Halbwachs, P. Lagnier, and . Raymond, Synchronous Observers and the Verification of Reactive Systems, Algebraic Methodology and Software Technology (AMAST'93), pp.83-96, 1994.
DOI : 10.1007/978-1-4471-3227-1_8

J. Henry, D. Monniaux, and M. Moy, PAGAI: A Path Sensitive Static Analyser, Electronic Notes in Theoretical Computer Science, vol.289, pp.15-25, 2012.
DOI : 10.1016/j.entcs.2012.11.003

J. Henry, D. Monniaux, and M. Moy, Succinct Representations for Abstract Interpretation, Static Analysis, pp.283-299, 2012.
DOI : 10.1007/978-3-642-33125-1_20
URL : https://hal.archives-ouvertes.fr/hal-00709833

T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic model checking for real-time systems, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.394-406, 1992.
DOI : 10.1109/LICS.1992.185551

]. C. Hoa69 and . Hoare, An Axiomatic Basis for Computer Programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.

Y. [. Halbwachs, P. Proy, and . Roumanoff, Verification of Real-Time Systems using Linear Relation Analysis, Formal Methods in System Design, vol.11, issue.2, pp.157-18510, 1997.
DOI : 10.1023/A:1008678014487

P. [. Irigoin, R. Jouvelot, and . Triolet, Semantical Interprocedural Parallelization: An Overview of the PIPS Project, pp.244-251, 1991.
URL : https://hal.archives-ouvertes.fr/hal-00984684

[. Inria, The Coq Proof Assistant, 1989.

]. B. Jea00 and . Jeannet, Partitionnement dynamique dans l'analyse de relation linéaire et application à la vérification de programmes synchrones, 2000.

]. B. Jea03 and . Jeannet, Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems. Formal Methods in System Design, pp.5-3710, 2003.

]. B. Jea10 and . Jeannet, The NBAC Verification/Slicing Tool, 2010.

]. L. Joh98 and . Johnson, DO-178B, Software Considerations in Airborne Systems and Equipment Certification, Crosstalk, 1998.

]. P. Jor06 and . Jordan, Standard IEC 62304 ? Medical Device Software ? Software Lifecycle Processes, Software for Medical Devices, pp.41-47, 2006.

]. M. Kar76 and . Karr, Affine Relationships among Variables of a Program, Acta Informatica, vol.6, issue.2, pp.133-15110, 1976.

. H. Kew-+-85-]-r, S. J. Katz, D. A. Eggers, C. L. Wood, R. G. Perkins et al., Implementing a Cache Consistency Protocol, ACM SIGARCH Computer Architecture News, vol.13, issue.3, pp.276-283, 1985.

]. D. Kha13 and . Khaldi, Parallélisation automatique et statique de tâches sous contraintes de ressources : une approche générique, 2013.

É. Cachan, FAST: Fast Acceleration of Symbolic Transition systems, 2003.

L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, vol.3, issue.2, pp.125-143, 1977.
DOI : 10.1109/TSE.1977.229904

]. L. Lam80 and . Lamport, Sometimee is Sometimes Not Neverr: On the Temporal Logic of Programs, pp.174-185, 1980.

]. C. Lee02 and . Lee, Program Termination Analysis in Polynomial Time, In Generative Programming and Component Engineering, vol.2487, pp.218-235, 2002.

B. [. Loechner, P. Meister, and . Clauss, Precise Data Locality Optimization of Nested Loops, The Journal of Supercomputing, vol.21, issue.1, pp.37-76, 2002.
DOI : 10.1023/A:1013535431127
URL : https://hal.archives-ouvertes.fr/inria-00534831

[. Verge, A Note on Chernikova's Algorithm, 1994.

]. A. Lya92 and . Lyapunov, The General Problem of the Stability of Motion. Control Theory and Applications Series, 1992.

]. V. Mai12 and . Maisonneuve, Convex Invariant Refinement by Control Node Splitting: A Heuristic Approach, Electronic Notes in Theoretical Computer Science, vol.288, pp.49-59, 2012.

]. D. Mas14 and . Massé, Policy Iteration-Based Conditional Termination and Ranking Functions, Verification, Model Checking, and Abstract Interpretation, pp.453-471, 2014.

]. N. Mer92 and . Mercouroff, An Algorithm for Analyzing Communicating Processes, Mathematical Foundations of Programming Semantics, pp.312-325

]. D. Mer05 and . Merchat, Réduction du nombre de variables en analyse de relations linéaires, 2005.

]. A. Min06 and . Miné, The Octagon Abstract Domain. Higher-Order and Symbolic Computation, pp.31-100, 2006.

[. Misra, Guidelines for the Use of the C Language in Vehicle Based Software, 1998.

T. Motzkin, H. Raiffa, G. L. Thompson, and R. M. , 3. The Double Description Method, Contributions to the Theory of Games II, 1953.
DOI : 10.1515/9781400881970-004

]. P. Ner13 and . Neron, A Quest for Exactness: Program Transformation for Reliable Real Numbers, Ecole Polytechnique X, 2013.

F. [. Nguyen and . Irigoin, Efficient and effective array bound checking, ACM Transactions on Programming Languages and Systems, vol.27, issue.3, pp.527-570, 2005.
DOI : 10.1145/1065887.1065893

F. [. Nguyen, C. Irigoin, R. Ancourt, and . Keryell, Efficient Intraprocedural Array Bound Checking, Second International Workshop on Automated Program Analysis, Testing and Verification, 2001.

T. [. Nookala and . Risset, A Library for Z-Polyhedral Operations, 2000.

C. Popeea and W. Chin, Inferring Disjunctive Postconditions, Advances in Computer Science -ASIAN 2006. Secure Software and Related Issues, pp.331-345, 2007.
DOI : 10.1007/11823230_2
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.135.7142

]. D. Pel01 and . Peled, Software Reliability Methods, 2001.

T. [. Paulson, M. Nipkow, and . Wenzel, The Isabelle theorem prover, pp.2002-2014

A. [. Podelski and . Rybalchenko, A Complete Method for the Synthesis of Linear Ranking Functions, Verification, Model Checking, and Abstract Interpretation, pp.239-251, 2004.
DOI : 10.1007/978-3-540-24622-0_20

]. W. Prk-+-14, E. Pugh, W. Rosser, D. Kelly, T. Wonnacot et al., The Omega Project, 1995.

G. [. Pelletier, C. Sutcliffe, and . Suttner, The Development of CASC, AI Communications, vol.15, issue.2-3, pp.79-90, 2002.

J. [. Queille and . Sifakis, Specification and verification of concurrent systems in CESAR, International Symposium on Programming, pp.337-351, 1982.
DOI : 10.1007/3-540-11494-7_22

[. Rtca, Software Considerations in Airborne Systems and Equipment Certification, 1992.

C. [. Sutcliffe and . Suttner, The State of CASC, AI Communications, vol.19, issue.1, pp.35-48, 2006.

]. G. Sut09 and . Sutcliffe, The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0, Journal of Automated Reasoning, vol.43, issue.4, pp.337-36210, 2009.

A. [. Verdoolaege, A. Cohen, and . Beletska, Transitive Closures of Affine Integer Tuple Relations and Their Overapproximations, Proceedings of the 18th International Conference on Static Analysis, pp.216-232, 2011.
DOI : 10.1007/978-3-642-02658-4_44
URL : https://hal.archives-ouvertes.fr/hal-00645221

]. S. Ver10 and . Verdoolaege, isl: An Integer Set Library for the Polyhedral Model, Mathematical Software ? ICMS 2010, pp.299-302, 2010.

S. Verdoolaege, R. Seghir, K. Beyls, V. Loechner, and M. Bruynooghe, Counting Integer Points in Parametric Polytopes Using Barvinok's Rational Functions, Algorithmica, vol.48, issue.1, pp.37-66, 2007.
DOI : 10.1007/s00453-006-1231-0

K. [. Verdoolaege, M. Woods, R. Bruynooghe, and . Cools, Computation and Manipulation of Enumerators of Integer Projections of Parametric Polytopes, 2005.

. Wdd-+-12-]-v, R. Wiels, D. Delmas, P. Doose, J. Garoche et al., Formal Verification of Critical Aerospace Software, AerospaceLab Journal, 2012.

D. K. Wilde, A LIBRARY FOR DOING POLYHEDRAL OPERATIONS, Parallel Algorithms and Applications, vol.15, issue.3-4, 1993.
DOI : 10.1007/BF02574699
URL : https://hal.archives-ouvertes.fr/inria-00074515

]. J. Yos13 and . Yoshida, Toyota Case: Single Bit Flip That Killed, EE Times, 2013.

. Venn, . Of, and .. For, 99 List of Tables 8.1 List of models currently provided with, terms of sets . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

.. Source-code-in-fsm-format and P. With, 88 8.2 C code produced by fsm2c for the example of Listing 8 91 8.3 iscc code produced by fsm2iscc for the example of Listing 8 92 10.1 Statements for counter 102 10.2 Transformers for counter, 109 10.8 Loop invariants for Listing 10.7 obtained iteratively when flag != 0 . . . . . . . 109 10.9 Periodic behavior10Loop invariants and postconditions for Listing 10.9 . . . . . . . . . . . . . . . . . 111 10.11While-if to while-while conversion: Example by Massé et, pp.10-112