Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

Abstract

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 
prove termination of JBC automatically. In this paper, we improve
this approach substantially in two ways:

(1) We extend it in order to also analyze recursive JBC programs. 
    To this end, one has to represent call stacks of arbitrary
    size.

(2) To handle JBC programs with several methods, we modularize our
    approach in order to re-use termination graphs and TRSs for the 
    separate methods and to prove termination of the resulting TRS 
    in a modular way.

We implemented our approach in the tool AProVE. Our experiments show 
that the new contributions increase the power of termination analysis 
for JBC significantly.