Termination Graphs for Java Bytecode

  • Marc Brockschmidt ,
  • Carsten Otto ,
  • Christian von Essen ,
  • Juergen Giesl

Verification, Induction, Termination Analysis |

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.