Skip to main content
SpringerLink
Log in

COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode

  • Conference paper
Formal Methods for Components and Objects (FMCO 2007)

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

Included in the following conference series:

Abstract

This paper describes the architecture of costa, an abstract interpretation based cost and termination analyzer for Java bytecode. The system receives as input a bytecode program, (a choice of) a resource of interest and tries to obtain an upper bound of the resource consumption of the program. costa provides several non-trivial notions of cost, as the consumption of the heap, the number of bytecode instructions executed and the number of calls to a specific method. Additionally, costa tries to prove termination of the bytecode program which implies the boundedness of any resource consumption. Having cost and termination together is interesting, as both analyses share most of the machinery to, respectively, infer cost upper bounds and to prove that the execution length is always finite (i.e., the program terminates). We report on experimental results which show that costa can deal with programs of realistic size and complexity, including programs which use Java libraries. To the best of our knowledge, this system provides for the first time evidence that resource usage analysis can be applied to a realistic object-oriented, bytecode programming language.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination Analysis of Java Bytecode. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 2–18. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 221–237. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Java Bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Removing Useless Variables in Cost Analysis of Java Bytecode. In: Proc. SAC. ACM Press, New York (2008)

    Google Scholar 

  5. Albert, E., Genaim, S., Gomez-Zamalloa, M.: Heap Space Analysis for Java Bytecode. In: ISMM 2007 (October 2007)

    Google Scholar 

  6. Allen, F.: Control flow analysis. In: Proceedings of a symposium on Compiler optimization, pp. 1–19 (1970)

    Google Scholar 

  7. Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile Resource Guarantees for Smart Devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 1–26. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Chander, A., Espinosa, D., Islam, N., Lee, P., Necula, G.: Enforcing resource bounds via static verification of dynamic checks. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 311–325. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming 41(1), 103–123 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  11. Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL 1977, pp. 238–252. ACM, New York (1977)

    Google Scholar 

  12. Crary, K., Weirich, S.: Resource Bound Certification. In: POPL 2000, pp. 184–198. ACM, New York (2000)

    Google Scholar 

  13. Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. TOPLAS 13(4) (1991)

    Google Scholar 

  14. Debray, S.K., Lin, N.W.: Cost analysis of logic programs. TOPLAS 15(5) (1993)

    Google Scholar 

  15. Goodrich, M.T., Tamassia, R.: Data Structures and Algorithms in Java, 3rd edn. John Wiley, Chichester (2004)

    MATH  Google Scholar 

  16. Hermenegildo, M., Albert, E., López-García, P., Puebla, G.: Abstraction Carrying Code and Resource-Awareness. In: Proc. of PPDP 2005. ACM Press, New York (2005)

    Google Scholar 

  17. Hermenegildo, M., Puebla, G., Bueno, F., López García, P.: Integrated Program Debugging, Verification, and Optimization Using Abstract Interpretation (and The Ciao System Preprocessor). Science of Comp. Progr. 58(1–2) (2005)

    Google Scholar 

  18. Hill, P.M., Payet, E., Spoto, F.: Path-length analysis of object-oriented programs. In: EAAI 2006, ENTS. Elsevier, Amsterdam (2006)

    Google Scholar 

  19. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL 2001, pp. 81–92. ACM, New York (2001)

    Google Scholar 

  20. Lehner, H., Müller, P.: Formal translation of bytecode into BoogiePL. In: Bytecode 2007, ENTCS, pp. 35–50. Elsevier, Amsterdam (2007)

    Google Scholar 

  21. Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley, Reading (1996)

    Google Scholar 

  22. Necula, G.: Proof-Carrying Code. In: POPL 1997, pp. 106–119. ACM Press, New York (1997)

    Google Scholar 

  23. Sands, D.: A naïve time analysis and its theory of cost equivalence. Journal of Logic and Computation 5(4) (1995)

    Google Scholar 

  24. Spoto, F.: Julia: A generic static analyser for the java bytecode. In: FTfJP 2005. (2005)

    Google Scholar 

  25. Spoto, F., Jensen, T.: Class analyses as abstract interpretations of trace semantics. ACM Trans. Program. Lang. Syst. 25(5), 578–630 (2003)

    Article  Google Scholar 

  26. Zou, W., Wei, T., Mao, J., Chen, Y.: A new algorithm for identifying loops in decompilation. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 170–183. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  27. Tip, F.: A Survey of Program Slicing Techniques. J. of Prog. Lang. 3 (1995)

    Google Scholar 

  28. Vallee-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a Java optimization framework. In: CASCON 1999, pp. 125–135 (1999)

    Google Scholar 

  29. Wegbreit, B.: Mechanical Program Analysis. Comm. of the ACM 18(9) (1975)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DSIC, Complutense University of Madrid, E-28040, Madrid, Spain

    Elvira Albert & Puri Arenas

  2. CLIP, Technical University of Madrid, E-28660, Boadilla del Monte, Madrid, Spain

    Samir Genaim, German Puebla & Damiano Zanardini

Authors
  1. Elvira Albert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Puri Arenas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Samir Genaim
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. German Puebla
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Damiano Zanardini
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Centre for Mathematics and Computer Science, CWI,, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

    Frank S. de Boer

  2. Leiden Institute of Advanced Computer Science, Leiden University, P.O. Box 9512, 2300 RA, Leiden, The Netherlands

    Marcello M. Bonsangue

  3. VERIMAG, 2 Avenue de Vignate, Centre Equitation,, 38610, Grenoble-Gières, France

    Susanne Graf

  4. Institute of Computer Science and Applied Mathematics, Christian-Albrechts University, Kiel,Hermann-Rodewald-Straße 3, 24118, Kiel, Germany

    Willem-Paul de Roever

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D. (2008). COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2007. Lecture Notes in Computer Science, vol 5382. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92188-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-92188-2_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-92187-5

  • Online ISBN: 978-3-540-92188-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation