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.
CITATION STYLE
Frohn, F., & Giesl, J. (2017). Complexity analysis for Java with AProVE. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10510 LNCS, pp. 85–101). Springer Verlag. https://doi.org/10.1007/978-3-319-66845-1_6
Mendeley helps you to discover research relevant for your work.