Proving Termination of Heap-Manipulating Java Programs

Automated termination analysis of imperative programs has seen great improvements in the past few years, but many of the presented methods are restricted to integer programs. As consequence, we developed symbolic evaluation graphs for Java programs, a finite over-approximation of all possible program runs of heap-manipulating Java programs, to remove this restriction. The graphs are obtained by symbolic evaluation using a simple abstract domain and can serve as basis for a range of further analyses and post-processing techniques. One such use, termination analysis by a sound transformation to Integer Term Rewriting, will be discussed in detail.