Experiments with Non-Termination Analysis for Java Bytecode

Non-termination analysis proves that programs, or parts of a program, do notterminate. This is important since non-termination is often an unexpectedbehaviour of computer programs and exposes a bug in their code.While research has found ways of proving non-termination of logic programsand of term rewriting systems, this is hardly the case for imperative programs.In this paper, we describe and experiment with a technique for provingnon-termination of imperative, bytecode programs by relating theirnon-termination to that of a (constraint) logic program. Moreover, we showthat our non-termination test effectively helps a termination test,by avoiding expensive search for termination proofs of thoseportions of the code where such proofs do not exist.