AIB 2017-04: Complexity Analysis for Java with AProVE

The following technical report is available from http://aib.informatik.rwth-aachen.de:

Complexity Analysis for Java with AProVE Florian Frohn and Jürgen Giesl AIB 2017-04

While AProVE is one of the most powerful tools for termination analysis of Java since many years, we now extend our approach in order to analyze the complexity of Java programs as well. Based on a symbolic execution of the program, we develop a novel transformation of (possibly heap-manipulating) Java programs to integer transition systems (ITSs). This allows us to use existing complexity analyzers for ITSs to infer runtime bounds for Java programs. We demonstrate the power of our implementation on an established standard benchmark set.