Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

Marc Brockschmidt, Carsten Otto & Jürgen Giesl
In earlier work we presented an approach to prove termination of non-recursive Java Bytecode (JBC) programs automatically. Here, JBC programs are first transformed to finite termination graphs which represent all possible runs of the program. Afterwards, the termination graphs are translated to term rewrite systems (TRSs) such that termination of the resulting TRSs implies termination of the original JBC programs. So in this way, existing techniques and tools from term rewriting can be used to...