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

C. Ancourt, F. Coelho, and F. 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

S. Bardin, Vers un Model Checking avec accélération plate des systèmes hétérogènes, 2005.

S. Bardin, A. Finkel, and J. 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

D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, Path invariants. page 300, 2007.
DOI : 10.1145/1273442.1250769

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

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

A. Michael, H. B. Colón, and . Sipma, Synthesis of linear ranking functions Tools and Algorithms for the Construction and Analysis of Systems, pp.67-81, 2001.

A. Michael, H. B. Colón, and . Sipma, Practical methods for proving program termination, Computer Aided Verification, pp.442-454, 2002.

B. Cook, A. Podelski, and A. Rybalchenko, Termination proofs for systems code, ACM SIGPLAN Notices, vol.41, issue.6, p.415, 2006.
DOI : 10.1145/1133255.1134029

P. Cousot, Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming
DOI : 10.1007/978-3-540-30579-8_1

G. Vardi, R. Weikum, and . Cousot, Verification, Model Checking, and Abstract Interpretation, pp.1-24, 2005.

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

P. Feautrier and L. 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

L. Gonnord, Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires, 2007.

D. Gopan and T. Reps, Lookahead Widening
DOI : 10.1007/11817963_41

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

S. Bhargav, T. A. Gulavani, Y. Henzinger, A. V. Kannan, S. K. Nori et al., SYNERGY: a new algorithm for property checking, p.117, 2006.

S. Gulwani, T. Speed-david-hutchison, J. Kanade, J. M. Kittler, F. Kleinberg et al., SPEED: Symbolic Complexity Bound Analysis, Computer Aided Verification, pp.51-62, 2009.
DOI : 10.1007/978-3-642-02658-4_7

S. Gulwani, S. Jain, and E. 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

S. Gulwani, K. K. Mehra, and T. Chilimbi, SPEED: precise and efficient static estimation of program computational complexity, p.127, 2008.

S. Gulwani and F. Zuleger, The reachability-bound problem. page 292, 2010.

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

N. Halbwachs, Delay analysis in synchronous programs, Computer Aided Verification, pp.333-346, 1993.
DOI : 10.1007/3-540-56922-7_28

N. Halbwachs, Linear relation analysis principles and recent progress, 2010.

N. Halbwachs, Y. Proy, and P. Roumanoff, Verification of real-time systems using linear relation analysis, Formal Methods in System Design, vol.11, issue.2, pp.157-185, 1997.
DOI : 10.1023/A:1008678014487

J. Henry, Static analysis by abstract interpretation, path focusing, 2011.

T. A. Henzinger and R. Jhala, Rupak Majumdar, and Grégoire Sutre. Lazy abstraction, pp.58-70, 2002.

B. Jeannet, Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems, Formal Methods in System Design, vol.23, issue.1, pp.5-37, 2003.
DOI : 10.1023/A:1024480913162

B. Jeannet, Partitionnement dynamique dans l'Analyse de Relation Linéaire et application à la vérification de programmes synchrones, 2000.

R. H. Katz, S. J. Eggers, D. A. Wood, C. L. Perkins, and R. G. Sheldon, Implementing a cache consistency protocol, ACM SIGARCH Computer Architecture News, vol.13, issue.3, pp.276-283, 1985.
DOI : 10.1145/327070.327237

L. Spécification, . Vérification, and . Éns-cachan, FAST -fast acceleration of symbolic transition systems, 2006.

L. Chin-soon, Program termination analysis in polynomial time, Generative Programming and Component Engineering, pp.218-235, 2002.

V. Maisonneuve, Convex Invariant Refinement by Control Node Splitting: a Heuristic Approach, Electronic Notes in Theoretical Computer Science, vol.288, pp.49-59, 2012.
DOI : 10.1016/j.entcs.2012.10.007
URL : https://hal.archives-ouvertes.fr/hal-00833344

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

F. J. Pelletier, G. Sutcliffe, and C. B. Suttner, The development of CASC, AI Communications, vol.15, issue.2-3, pp.79-90, 2002.

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

C. Popeea, W. Hutchison, T. Kanade, J. Kittler, J. M. Kleinberg et al., Inferring Disjunctive Postconditions, Advances in Computer Science -ASIAN 2006. Secure Software and Related Issues, pp.331-345
DOI : 10.1007/11823230_2
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.135.7142

W. Pugh, The omega project, 2011.

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

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

S. Verdoolaege, D. Hutchison, T. Kanade, J. Kittler, J. M. Kleinberg et al., isl: An Integer Set Library for the Polyhedral Model, Mathematical Software ? ICMS 2010, pp.299-302
DOI : 10.1007/978-3-642-15582-6_49