Proving Termination of Heap-Manipulating Java Programs
Marc Brockschmidt ( MSR Cambridge )
- 11:30 29th November 2012 ( week 8, Michaelmas Term 2012 )278
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.