The following technical report is available from http://aib.informatik.rwth-aachen.de:

Automated Termination Analysis of Java Bytecode by Term Rewriting Carsten Otto, Marc Brockschmidt, Christian von Essen, Jürgen Giesl AIB 2010-08

We present an automated approach to prove termination of Java Bytecode (JBC) programs by automatically transforming them to term rewrite systems (TRSs). In this way, the numerous techniques and tools developed for TRS termination can now be used for imperative object-oriented languages like Java, which can be compiled into JBC.