[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Complexity Analysis for Java with AProVE

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10510))

Included in the following conference series:

Abstract

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.

Support by DFG grant GI 274/6-1 and the Air Force Research Laboratory (AFRL).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    See http://www.termination-portal.org/wiki/Termination_Competition and http://sv-comp.sosy-lab.org.

  2. 2.

    The work on worst-case execution time (WCET) for real-time systems [25] is largely orthogonal to the inference of symbolic loop bounds.

  3. 3.

    We presented a preliminary extended abstract with our “size” definition at the 15th Int. Workshop on Termination, an informal workshop without formal reviewing or published proceedings, cf. http://cl-informatik.uibk.ac.at/events/wst-2016.

  4. 4.

    The TPDB is the collection of examples used for the annual Termination Competition, available from http://termination-portal.org/wiki/TPDB.

  5. 5.

    As we do not regard floats, JBC represents all primitive Java types as integers.

  6. 6.

    For the sake of simplicity, we assume that all states are well typed throughout this paper, i.e., local variables of type int always store symbolic integers, etc.

  7. 7.

    With this notion of size, the transformation from objects to terms that we used for termination analysis in [22] is unsound for complexity analysis, as it duplicates objects that can be reached by different fields: Consider a binary “tree” of n nodes where the left and right child of each inner node are the same. The size \(\Vert \cdot \Vert \) of this object is linear in n, but the resulting transformed term would be exponential in n. This problem is avoided by our new transformation to integers instead of terms in Sect. 3.

  8. 8.

    The descriptor specifies the argument types and return type of a method (“LList;” stands for the argument type List and “I” stands for the result type int), see docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.3.3.

  9. 9.

    While s may have the predicate , it cannot contain \(\widehat{o} =^{?} o\), as our symbolic execution rules require that if a field of o is written by putfield, then predicates of the form \(\widehat{o} =^{?} o\) first have to be removed by refinement steps, cf. [5]. Similarly, \(o \in \mathsf {Dom}(h)\) is enforced by refinements before symbolically evaluating putfield.

  10. 10.

    Java2Jinja (http://pp.ipd.kit.edu/projects/quis-custodiet/Java2Jinja) generates JinjaThreads-code, which is a superset of Jinja and cannot be handled by [4].

  11. 11.

    We could not adapt Julia_10_Iterative/RSA as its sources are missing.

References

  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)

    Article  MathSciNet  MATH  Google Scholar 

  2. AProVE. https://aprove-developers.github.io/jbc-complexity/

  3. Atkey, R.: Amortised resource analysis with separation logic. Logical Methods Comput. Sci. 7(2) (2011)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  9. Complexity Analysis-Based Guaranteed Execution. http://www.draper.com/news/draper-s-cage-could-spot-code-vulnerable-denial-service-attacks

  10. Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proceedings of the PLDI 2015, pp. 467–478 (2015)

    Google Scholar 

  11. Debray, S., Lin, N.-W.: Cost analysis of logic programs. ACM TOPLAS 15(5), 826–875 (1993)

    Article  Google Scholar 

  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. 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

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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

    Chapter  Google Scholar 

  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. 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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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)

    Article  MathSciNet  MATH  Google Scholar 

  24. Space/Time Analysis for Cybersecurity (STAC). http://www.darpa.mil/program/space-time-analysis-for-cybersecurity

  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 

Download references

Author information

Authors and Affiliations

  1. LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

    Florian Frohn & Jürgen Giesl

Authors
  1. Florian Frohn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jürgen Giesl
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jürgen Giesl .

Editor information

Editors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, Massachusetts, USA

    Nadia Polikarpova

  2. University of Surrey, Guildford, United Kingdom

    Steve Schneider

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Frohn, F., Giesl, J. (2017). Complexity Analysis for Java with AProVE . In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66845-1_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66844-4

  • Online ISBN: 978-3-319-66845-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation