Skip to main content
SpringerLink
Log in

Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4349))

Abstract

We introduce Cibai a generic static analyzer based on abstract interpretation for the modular analysis and verification of Java classes. We present the abstract semantics and the underlying abstract domain, a combination of an aliasing analysis and octagons. We discuss some implementation issues, and we compare Cibai with similar tools, showing how Cibai achieves a higher level of automation and precision while having comparable performances.

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. JUnit: http://junit.sourceforge.net/

  2. Aggarwal, A., Randall, K.H: Related field analysis. In: PLDI (2001)

    Google Scholar 

  3. Barnett, M., Leino, K.R.M, Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., et al. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 10–14. Springer, Heidelberg (2005)

    Google Scholar 

  4. Blanchet, B.: Escape Analysis: Correctness proof, implementation and experimental results. In: POPL (1998)

    Google Scholar 

  5. Cok, D.R, Kiniry, J.: ESC/Java 2: Uniting ESC/Java and JML. In: CASSIS (2004)

    Google Scholar 

  6. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)

    Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation, 2(4) (August 1992)

    Google Scholar 

  8. Ernst, M.D: Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington (2000)

    Google Scholar 

  9. Ferrara, P.: JAIL: Firewall analysis of JavaCard by Abstract Interpretation. In: EAAI (2006)

    Google Scholar 

  10. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. Sun Microsystems (2001)

    Google Scholar 

  11. Henkel, J., Diwan, A.: Discovering algebraic specifications from java classes. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, Springer, Heidelberg (2003)

    Google Scholar 

  12. Jacobs, B., van den Berg, J., Huismann, H., van Berkum, M., Hensel, U., Tews, H. Reasoning about Java classes (preliminary report). In: OOPSLA (1998)

    Google Scholar 

  13. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary Design of JML: A Behavioral Interface Specification Language for Java (November 2003)

    Google Scholar 

  14. Logozzo, F.: Separate compositional analysis of class-based object-oriented languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, Springer, Heidelberg (2004)

    Google Scholar 

  15. Logozzo, F.: Modular Static Analysis of Object-oriented languages. PhD thesis, École Polytecnique (2004)

    Google Scholar 

  16. Logozzo, F.: Class invariants as abstract interpretation of trace semantics. Computer Languages, Systems and Structures (2007)

    Google Scholar 

  17. Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java/Javacard programs. Annotated in JML. J. Log. Algebr. Program, 58(1–2) (2004)

    Google Scholar 

  18. Meyer., B.: Object-Oriented Software Construction. In: Professional Technical Reference, 2nd edn., Prentice Hall, Englewood Cliffs (1997)

    Google Scholar 

  19. Miné, A.: The octagon abstract domain. In: AST (2001)

    Google Scholar 

  20. Pollet, I., Le Charlier, B., Cortesi, A.: Distinctness and sharing domains for static analysis of Java programs. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  21. Rossignoli, S., Spoto, F.: Detecting Non-Cyclicity by Abstract Compilation into Boolean Functions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Google Scholar 

  23. Everest Team: Jack, Java Applet Correctness Kit, http://www-sop.inria.fr/everest/soft/Jack/jack.html

  24. Tillmann, N., Chen, F., Schulte, W.: Discovering likely method specifications. Technical report, Microsoft Research (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École Normale Supérieure, 45, rue d’Ulm, Paris, France

    Francesco Logozzo

Authors
  1. Francesco Logozzo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Byron Cook Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Logozzo, F. (2007). Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes. In: Cook, B., Podelski, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2007. Lecture Notes in Computer Science, vol 4349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69738-1_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-69738-1_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69735-0

  • Online ISBN: 978-3-540-69738-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation