A Termination Analyzer for Java Bytecode based on Path-Length

It is important to prove that supposedly terminating programs actuallyterminate, particularly if those programs must berun on critical systems or downloaded into a client such as a mobile phone.Although termination of computer programs is generally undecidable,it is possible and useful to provetermination of a large, non-trivial subset of the terminating programs.In this paper we present our termination analyser for sequential Java bytecode,based on a program property called path-length. We describe theanalyses which are needed before the path-length can be computed, such assharing, cyclicity and aliasing. Then weformally define the path-length analysis and prove it correct wrt areference denotational semantics of the bytecode. We show that a constraintlogic program P_CLPcan be built from the result of the path-length analysisof a Java bytecode program P andformally prove that if P_CLP terminates then also P terminates.Hence a termination prover for constraint logic programs can be appliedto prove the termination of P. We conclude with some discussion of thepossibilities and limitations of our approach.Ours is the first existing termination analyser for Java bytecodedealing with any kind of data structures dynamically allocated on the heapand which does not require any help or annotation on the part of the user.