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.