, Android -An Open Handset Alliance Project

R. N. Bol, K. R. Apt, and J. W. Klop, An analysis of loop checking mechanisms for logic programs, Theoretical Computer Science, vol.86, issue.1, pp.35-79, 1991.
DOI : 10.1016/0304-3975(91)90004-L

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/hal-01108790

D. Schreye, D. , K. Verschaetse, and M. Bruynooghe, A Practical Technique for Detecting non- Terminating Queries for a Restricted Class of Horn Clauses, using Directed, Weighted Graphs, Proc. of ICLP'90, pp.649-663, 1990.

J. Giesl, R. Thiemann, and P. Schneider-kamp, Proving and Disproving Termination of Higher-Order Functions, Proc. of the 5th International Workshop on Frontiers of Combining Systems (FroCoS'05), pp.216-231, 2005.
DOI : 10.1007/11559306_12

P. Godefroid, N. Klarlund, and K. Sen, DART: Directed Automated Random Testing, Proc. of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI'05) (2005), pp.213-223

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

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

E. Payet, Loop detection in term rewriting using the eliminating unfoldings, Theoretical Computer Science, vol.403, issue.2-3, pp.307-327, 2008.
DOI : 10.1016/j.tcs.2008.05.013
URL : https://hal.archives-ouvertes.fr/hal-01186183

E. Payet and F. Mesnard, Abstract, Theory and Practice of Logic Programming, vol.9, issue.02, 2008.
DOI : 10.1007/s10817-005-6545-0

E. Payet and F. Mesnard, Nontermination inference of logic programs, ACM Transactions on Programming Languages and Systems, vol.28, issue.2, pp.256-289, 2006.
DOI : 10.1145/1119479.1119481
URL : https://hal.archives-ouvertes.fr/hal-00129526

S. Rossignoli and F. Spoto, Detecting Non-cyclicity by Abstract Compilation into Boolean Functions, Proc. of the 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'06), pp.95-110, 2006.
DOI : 10.1007/11609773_7
URL : http://profs.sci.univr.it/~spoto/vmcai06_proofs.pdf.gz

S. Secci and F. Spoto, Pair-Sharing Analysis of Object-Oriented Programs, Proc. of Static Analysis Symposium (SAS'05), pp.320-335, 2005.
DOI : 10.1007/11547662_22
URL : http://profs.sci.univr.it/~spoto/sas05_extended.pdf.gz

K. Sen, D. Marinov, and G. Agha, CUTE: a Concolic Unit Testing Engine for C, Proc. of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp.263-272, 2005.
DOI : 10.21236/ada482657
URL : http://www.dtic.mil/dtic/tr/fulltext/u2/a482657.pdf

Y. Shen, J. You, L. Yuan, S. Shen, and Q. Yang, A dynamic approach to characterizing termination of general logic programs, ACM Transactions on Computational Logic, vol.4, issue.4, pp.417-434, 2003.
DOI : 10.1145/937555.937556
URL : http://arxiv.org/pdf/cs/0204031

Y. Shen, L. Yuan, and J. , Loop checks for logic programs with functions, Theoretical Computer Science, vol.266, issue.1-2, pp.441-461, 2001.
DOI : 10.1016/S0304-3975(00)00197-3
URL : https://doi.org/10.1016/s0304-3975(00)00197-3

F. Spoto, P. M. Hill, and E. Payet, Path-Length Analysis for Object-Oriented Programs, in: First International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), 2006.

F. Spoto, L. Lu, and F. Mesnard, Using CLP Simplifications to Improve Java Bytecode Termination Analysis, Electronic Notes in Theoretical Computer Science, vol.253, issue.5
DOI : 10.1016/j.entcs.2009.11.019
URL : https://hal.archives-ouvertes.fr/hal-01188704

F. Spoto, F. Mesnard, and E. Payet, A Termination Analyser for Java Bytecode Based on Path-Length, submitted for publication in, 2007.
DOI : 10.1145/1709093.1709095

H. Velroyen and P. Rümmer, Non-termination Checking for Imperative Programs, Proc. of the 2nd International Conference on Tests and Proofs (TAP'08), pp.154-170, 2008.
DOI : 10.1007/978-3-540-79124-9_11
URL : http://www.cs.chalmers.se/~philipp/publications/non-termination.pdf

J. Waldmann, Matchbox: A Tool for Match-Bounded String Rewriting, Proc. of the 15th International Conference on Rewriting Techniques and Applications, pp.85-94, 2004.
DOI : 10.1007/978-3-540-25979-4_6

J. Waldmann, Compressed Loops (draft), 2007.

H. Zankl and A. Middeldorp, Nontermination of String Rewriting using SAT, Proc. of the 9th International Workshop on Termination (WST'07), pp.52-55, 2007.

H. Zantema, Termination of String Rewriting Proved Automatically, Journal of Automated Reasoning, vol.33, issue.2, pp.105-139, 2005.
DOI : 10.1007/978-3-540-25979-4_7
URL : https://pure.tue.nl/ws/files/1729598/200314.pdf