Automated termination analysis is an important area in program
verification. While AProVE is one of the most powerful tools for
termination analysis of Java programs since many years, we now
extended our technique in order to analyze the complexity of Java
programs as well.
Our approach first executes the program symbolically on a
suitable abstract domain. Based on this symbolic execution, we
develop a novel transformation of (possibly heap-manipulating)
Java programs to integer transition systems (ITSs). This allows
us to apply existing complexity analyzers for standard ITSs in
order to infer runtime bounds for Java programs. We demonstrate
the power of our implementation on an established benchmark set.
Moreover, we give a general overview of the AProVE tool and show
how it can be used to analyze termination and complexity of
programs for several different programming paradigms.