Termination Graphs for Java Bytecode

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.

• Type: Journal
• Year: 2010
• Where: BIRTHDAY
• Authors: Marc Brockschmidt, Carsten Otto, Christian von Essen, Jürgen Giesl
• Keywords: Applied Computing, BIRTHDAY 2010, Original Jbc Program, Possible Runs, Termination Graph