Complexity Analysis for Java with AProVE

  • Florian Frohn
  • Jürgen GieslEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


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.


  1. 1.
    Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comp. Sci. 413(1), 142–159 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
  3. 3.
    Atkey, R.: Amortised resource analysis with separation logic. Logical Methods Comput. Sci. 7(2) (2011)Google Scholar
  4. 4.
    Avanzini, M., Moser, G., Schaper, M.: TcT: Tyrolean complexity tool. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 407–423. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49674-9_24 CrossRefGoogle Scholar
  5. 5.
    Brockschmidt, M., Otto, C., Essen, C., Giesl, J.: Termination graphs for Java Bytecode. In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis. LNCS, vol. 6463, pp. 17–37. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-17172-7_2 CrossRefGoogle Scholar
  6. 6.
    Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 105–122. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31424-7_13 CrossRefGoogle Scholar
  7. 7.
    Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387–393. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49674-9_22 CrossRefGoogle Scholar
  8. 8.
    Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM TOPLAS 38(4), 13:1–13:50 (2016)CrossRefGoogle Scholar
  9. 9.
  10. 10.
    Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proceedings of the PLDI 2015, pp. 467–478 (2015)Google Scholar
  11. 11.
    Debray, S., Lin, N.-W.: Cost analysis of logic programs. ACM TOPLAS 15(5), 826–875 (1993)CrossRefGoogle Scholar
  12. 12.
    Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275–295. Springer, Cham (2014). doi: 10.1007/978-3-319-12736-1_15 Google Scholar
  13. 13.
    Genaim, S., Codish, M., Gallagher, J., Lagoon, V.: Combining norms to prove termination. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 126–138. Springer, Heidelberg (2002). doi: 10.1007/3-540-47813-2_9 CrossRefGoogle Scholar
  14. 14.
    Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reasoning 58(1), 3–31 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: precise and efficient static estimation of program computational complexity. In: Proceedings of the POPL 2009, pp. 127–139 (2009)Google Scholar
  16. 16.
    Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 167–177. Springer, Heidelberg (1989). doi: 10.1007/3-540-51081-8_107 CrossRefGoogle Scholar
  17. 17.
    Hoffmann, J., Das, A., Weng, S.-C.: Towards automatic resource bound analysis for OCaml. In: Proceedings of the POPL 2017, pp. 359–373 (2017)Google Scholar
  18. 18.
    Hofmann, M., Rodriguez, D.: Automatic type inference for amortised heap-space analysis. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 593–613. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-37036-6_32 CrossRefGoogle Scholar
  19. 19.
    Ji, R., Hähnle, R., Bubel, R.: Program transformation based on symbolic execution and deduction. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 289–304. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-40561-7_20 CrossRefGoogle Scholar
  20. 20.
    Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM TOPLAS 28(4), 619–695 (2006)CrossRefGoogle Scholar
  21. 21.
    Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reasoning 51(1), 27–56 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proceedings of the RTA 2010, LIPIcs 6, pp. 259–276 (2010)Google Scholar
  23. 23.
    Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reasoning 59(1), 3–45 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Space/Time Analysis for Cybersecurity (STAC).
  25. 25.
    Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenström, P.: The worst-case execution-time problem - overview of methods and survey of tools. ACM TECS 7(3), 36:1–36:53 (2008)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.LuFG Informatik 2RWTH Aachen UniversityAachenGermany

Personalised recommendations