Termination Graphs for Java Bytecode

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

Abstract

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.

Details

Publication typeInproceedings
Published inVerification, Induction, Termination Analysis
> Publications > Termination Graphs for Java Bytecode