A. V. Aho, R. Sethi, and J. D. Ullman, Compilers, Principles Techniques and Tools, 1986.

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini, Removing useless variables in cost analysis of Java bytecode, Proceedings of the 2008 ACM symposium on Applied computing , SAC '08, pp.368-375, 2008.
DOI : 10.1145/1363686.1363779

A. M. Ben-amram and M. Codish, A SAT-Based Approach to Size Change Termination with Global Ranking Functions, Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), pp.218-232, 2008.
DOI : 10.1007/978-3-540-78800-3_16

J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. W. O-'hearn, Variance Analyses from Invariance Analyses, Proc. of the 34th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL'07), pp.211-224, 2007.

J. Berdine, B. Cook, D. Distefano, and P. W. O-'hearn, Automatic Termination Proofs for Programs with Shape-Shifting Heaps, Proc. of the 18th International Conference on Computer Aided Verification (CAV'06), pp.386-400, 2006.
DOI : 10.1007/11817963_35

A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro et al., Programs with Lists Are Counter Automata, Proc. of the 18th International Conference on Computer Aided Verification (CAV'06), pp.517-531, 2006.
DOI : 10.1007/11817963_47

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

M. Codish, Proving Termination with (Boolean) Satisfaction, Proc. of the 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'07), pp.1-7, 2007.
DOI : 10.1007/978-3-540-73449-9_29

M. Codish and C. Taboch, A semantic basis for the termination analysis of logic programs, The Journal of Logic Programming, vol.41, issue.1, pp.103-123, 1999.
DOI : 10.1016/S0743-1066(99)00006-0

B. Cook, A. Podelski, and A. Rybalchenko, Terminator: Beyond Safety, Proc. of the 18th International Conference on Computer Aided Verification, pp.415-418, 2006.
DOI : 10.1007/11817963_37

S. Genaim and M. Codish, Inferring termination conditions for logic programs using backwards analysis, Theory and Practice of Logic Programming, vol.5, issue.1-2, pp.75-91, 2005.
DOI : 10.1017/S1471068404002236

J. Giesl, P. Schneider-kamp, and R. Thiemann, AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework, 3th International Joint Conference on Automated Reasoning, pp.281-286, 2006.
DOI : 10.1007/11814771_24

T. Lindholm and F. Yellin, The Java TM Virtual Machine Specification, 1999.

A. Loginov, T. W. Reps, and M. Sagiv, Refinement-Based Verification for Possibly-Cyclic Lists, Proc. of Theory and Practice of Program Analysis and Compilation, Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, pp.247-272, 2006.
DOI : 10.1007/978-3-540-71322-7_12

P. Manolios and D. Vroon, Termination Analysis with Calling Context Graphs, Proc. of the 18th International Conference on Computer Aided Verification, pp.401-414, 2006.
DOI : 10.1007/11817963_36

A. Podelski and A. Rybalchenko, Transition Predicate Abstraction and Fair Termination, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.29, issue.3, 2007.

F. Spoto, P. M. Hill, and . Payet, Path-Length Analysis for Object-Oriented Programs, First International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), 2006.
URL : https://hal.archives-ouvertes.fr/hal-01915777

F. Spoto, F. Mesnard, and . Payet, A Termination Analyser for Java Bytecode Based on Path-Length. Submitted for publication in Available at the web address http, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01916989

A. Turing, On Computable Numbers, with an Application to the Entscheidungsproblem, pp.230-265, 1936.