P. A. Abdulla, A. Collomb-annichini, A. Bouajjani, and B. Jonsson, Using Forward Reachability Analysis for Verification of Lossy Channel Systems, Formal Methods in System Design, vol.25, issue.1, pp.39-65, 2004.
DOI : 10.1023/B:FORM.0000033962.51898.1a

R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho et al., The algorithmic analysis of hybrid systems, Theoretical Computer Science, vol.138, issue.1, pp.3-34, 1995.
DOI : 10.1016/0304-3975(94)00202-T

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

R. Bagnara, K. Dobson, P. M. Hill, M. Mundell, and E. Zaffanella, Grids: A domain for analyzing the distribution of numerical values. In: Logic-Based Program Synthesis and Transformation, LOPSTR'06, LNCS, vol.4407, pp.219-235, 2006.

S. Bardin, A. Finkel, and J. Leroux, FASTer Acceleration of Counter Automata in Practice, LNCS, vol.2988, pp.576-590, 2004.
DOI : 10.1007/978-3-540-24730-2_42

S. Bardin, A. Finkel, J. Leroux, and L. Petrucci, FAST: Fast Acceleration of Symbolic Transition Systems, In: Computer Aided Verification. LNCS, vol.2725, pp.118-121, 2003.
DOI : 10.1007/978-3-540-45069-6_12
URL : https://hal.archives-ouvertes.fr/hal-00084185

S. Bardin, A. Finkel, J. Leroux, and P. Schnoebelen, Flat Acceleration in Symbolic Model Checking, In: Automated Technology for Verification and Analysis. LNCS, vol.3707, pp.474-488, 2005.
DOI : 10.1007/11562948_35
URL : https://hal.archives-ouvertes.fr/hal-00346302

A. Beletska, D. Barthou, W. Bielecki, and A. Cohen, Computing the Transitive Closure of a Union of Affine Integer Tuple Relations, In: Combinatorial Optimization and Applications. LNCS, vol.6508, pp.98-109, 2009.
DOI : 10.1007/978-3-642-02026-1_9
URL : https://hal.archives-ouvertes.fr/hal-00575959

F. Benoy, A. King, and F. Mesnard, Computing convex hulls with a linear solver, Theory and Practice of Logic Programming, vol.5, issue.1-2, pp.259-271, 2005.
DOI : 10.1017/S1471068404002261

B. Boigelot, Symbolic methods for exploring infinite state spaces, 1999.

B. Boigelot and P. Godefroid, Symbolic verification of communication protocols with infinite state spaces using QDDs, Formal Methods in System Design, vol.14, issue.3, pp.237-255, 1997.
DOI : 10.1007/3-540-61474-5_53

B. Boigelot and F. Herbreteau, The Power of Hybrid Acceleration, Computer Aided Verification, pp.438-451, 2006.
DOI : 10.1007/11817963_40
URL : https://hal.archives-ouvertes.fr/inria-00335905

B. Boigelot, F. Herbreteau, and S. Jodogne, Hybrid acceleration using real vector automata (extended abstract), Computer Aided Verification. LNCS, vol.2725, pp.193-205, 2003.

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

M. Bozga, R. Iosif, and F. Konecn´ykonecn´y, Fast Acceleration of Ultimately Periodic Relations, Computer Aided Verification. LNCS, vol.6174, pp.227-242, 2010.
DOI : 10.1007/978-3-642-14295-6_23
URL : https://hal.archives-ouvertes.fr/hal-01418908

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

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

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

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

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. Finkel and J. Leroux, How to Compose Presburger-Accelerations: Applications to Broadcast Protocols, Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.2556, pp.145-156, 2002.
DOI : 10.1007/3-540-36206-1_14

L. Fribourg and H. Olsén, Proving safety properties of infinite state systems by compilation into Presburger arithmetic, Conference on Concurrency Theory, pp.213-227, 1997.
DOI : 10.1007/3-540-63141-0_15

K. Fukuda and A. Prodon, Double description method revisited, Combinatorics and Computer Science. LNCS, 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

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

L. Gonnord, The ASPIC tool: Accelerated symbolic polyhedral invariant computation, 2009.

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. Granger, Static analysis of linear congruence equalities among variables of a program, TAPSOFT'91, pp.169-192, 1991.
DOI : 10.1007/3-540-53982-4_10

N. Halbwachs, F. Lagnier, and P. Raymond, Synchronous Observers and the Verification of Reactive Systems, Algebraic Methodology and Software Technology. Workshops in Computing, pp.83-96, 1993.
DOI : 10.1007/978-1-4471-3227-1_8

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

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, T. Jéron, V. Rusu, and E. Zinovieva, Symbolic Test Selection Based on Approximate Analysis, LNCS, vol.3440, pp.349-364, 2005.
DOI : 10.1007/978-3-540-31980-1_23
URL : https://hal.archives-ouvertes.fr/inria-00564617

N. D. Jones, C. Gomard, and P. Sestoft, Partial Evaluation and Automatic Program Generation, 1993.

J. B. Kam and J. D. Ullman, Monotone data flow analysis frameworks, Acta Informatica, vol.2, issue.3, pp.305-317, 1977.
DOI : 10.1007/BF00290339

J. Leroux, Algorithmique de la vérification des systèmessystèmesà compteurs ? approximation et accélération ? implémentation dans l'outil FAST, 2003.

J. Leroux and G. Sutre, Acceleration in Convex Data-Flow Analysis, In: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.4855, pp.520-531, 2007.
DOI : 10.1007/978-3-540-77050-3_43
URL : https://hal.archives-ouvertes.fr/hal-00346295

M. L. Minsky, Recursive Unsolvability of Post's Problem of "Tag" and other Topics in Theory of Turing Machines, The Annals of Mathematics, vol.74, issue.3, pp.437-455, 1961.
DOI : 10.2307/1970290

P. Schrammel and B. Jeannet, Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs, Electronic Notes in Theoretical Computer Science, vol.267, issue.1, pp.101-114, 2010.
DOI : 10.1016/j.entcs.2010.09.009
URL : https://hal.archives-ouvertes.fr/hal-00749914

P. Schrammel and B. Jeannet, Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs, Static Analysis Symposium, SAS'11, pp.233-248, 2011.
DOI : 10.1007/s10703-006-0031-0
URL : https://hal.archives-ouvertes.fr/inria-00596241