AIB 2010-15: Termination Graphs for Java Bytecode

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

Termination Graphs for Java Bytecode Marc Brockschmidt, Carsten Otto, Christian von Essen, Jürgen Giesl AIB 2010-15

To prove termination of Java Bytecode (JBC) automatically, we transform JBC to finite termination graphs which represent all possible runs of the program. Afterwards, the graph can be translated into "simple" formalisms like term rewriting and existing tools can be used to prove termination of the resulting term rewrite system (TRS). In this paper we show that termination graphs indeed capture the semantics of JBC correctly. Hence, termination of the TRS resulting from the termination graph implies termination of the original JBC program.