A. M. Ben-amram, Monotonicity constraints for termination in the integer domain, Logical Methods in Computer Science, vol.7, issue.3, 2011.

A. R. Bradley, Z. Manna, and H. B. Sipma, Termination of polynomial programs, Proc. of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), pp.113-129, 2005.

M. Braverman, Termination of integer linear programs, Proc. of the 18th International Conference on Computer Aided Verification (CAV'06), vol.4144, pp.372-385, 2006.

J. R. Büchi, On a decision method in restricted second-order arithmetic, Proc. of the 1960 International Congress on Logic, Methodology and Philosophy of Science (LMPS'60), pp.1-11, 1962.

H. Chen, B. Cook, C. Fuhs, K. Nimkar, and P. O'hearn, Proving nontermination via safety, Proc. of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), vol.8413, pp.156-171, 2014.

M. Codish, V. Lagoon, and P. Stuckey, Testing for termination with monotonicity constraints, Proc. of the 21st International Conference on Logic Programming (ICLP'05), vol.3668, pp.326-340, 2005.

D. De-schreye, M. Bruynooghe, and K. Verschaetse, On the existence of nonterminating queries for a restricted class of Prolog-clauses, Artificial Intelligence, vol.41, pp.237-248, 1989.

A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R. G. Xu, Proving non-termination, Proc. of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pp.147-158, 2008.

N. Klarlund and A. Møller, MONA Version 1.4 User Manual, 2001.

C. S. Lee, N. D. Jones, and A. M. Ben-amram, The size-change principle for program termination, Proc. of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), pp.81-92, 2001.

M. O. Rabin, Decidability of Second-Order Theories and Automata on Infinite Trees, Transactions of the American Mathematical Society, vol.141, pp.1-35, 1969.

F. Spoto, F. Mesnard, and . Payet, A termination analyzer for Java bytecode based on path-length, ACM Transactions on Programming Languages and Systems, vol.32, issue.3, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01186167

W. Thomas, Automata on infinite objects, Formal Models and Semantics, vol.B, pp.133-191, 1990.

A. Tiwari, Termination of linear programs, Proc. of the 16th International Conference on Computer Aided Verification (CAV'04), vol.3114, pp.70-82, 2004.