Termination Analysis of Java Bytecode

Abstract. Termination analysis has received considerable attention, tra-ditionally in the context of declarative programming, and recently also for imperative languages. In existing approaches, termination is per-formed on source programs. However, there are many situations, includ-ing mobile code, where only the compiled code is available. In this work we present an automatic termination analysis for sequential Java Byte-code programs. Such analysis presents all of the challenges of analyzing a low-level language as well as those introduced by object-oriented lan-guages. Interestingly, given a bytecode program, we produce a constraint logic program, CLP, whose termination entails termination of the byte-code program. This allows applying the large body of work in termination of CLP programs to termination of Java bytecode. A prototype analyzer is described and initial experimentation is reported.