Abstract
The Julia static analyzer applies abstract interpretation to the analysis and verification of Java bytecode. It is the result of 13 years of engineering effort based on theoretical research on denotational and constraint-based static analysis through abstract interpretation. Julia is a library for static analysis, over which many checkers have been built, that verify the absence of a large set of typical errors of software: among them are null-pointer accesses, non-termination, wrong synchronization and injection threats to security. This article recaps the history of Julia, describes the technology under the hood of the tool, reports lessons learned from the market, current limitations and future work.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In this article, bytecode refers both to the low-level language resulting from the compilation of Java and to each single instruction of that language. This is standard terminology, although possibly confusing.
References
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: 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, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 113–132. Springer, Heidelberg (2008)
Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)
Bagnara, R., Mesnard, F., Pescetti, A., Zaffanella, E.: A new look at the automatic synthesis of linear ranking functions. Inf. Comput. 215, 47–67 (2012)
Bryant, R.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)
Codish, M., Lagoon, V., Stuckey, P.J.: Testing for termination with monotonicity constraints. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 326–340. Springer, Heidelberg (2005)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of Principles of Programming Languages (POPL 1977), pp. 238–252 (1977)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
Ernst, M.D., Lovato, A., Macedonio, D., Spiridon, C., Spoto, F.: Boolean formulas for the static identification of injection attacks in Java. In: Davis, M., et al. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 130–145. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48899-7_10
Ernst, M.D., Lovato, A., Macedonio, D., Spoto, F., Thaine, J.: Locking discipline inference and checking. In: Proceedings of Software Engineering (ICSE 2016), Austin, TX, USA, pp. 1133–1144. ACM (2016)
Ernst, M.D., Macedonio, D., Merro, M., Spoto, F.: Semantics for locking specifications. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 355–372. Springer, Heidelberg (2016). doi:10.1007/978-3-319-40648-0_27
The Apache Software Foundation. Jasper 2 JSP Engine How To. https://tomcat.apache.org/tomcat-8.0-doc/jasper-howto.html
The Apache Software Foundation. Apache Commons BCEL. https://commons.apache.org/proper/commons-bcel. 24 June 2016
Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., Lea, D.: Java Concurrency in Practice. Addison Wesley, Reading (2006)
Göransson, A.: Efficient Android Threading. O’Reilly Media, Sebastopol (2014)
Red Hat. Hibernate. Everything Data. http://hibernate.org
Hermenegildo, M., Warren, D.S., Debray, S.K.: Global flow analysis as a practical compilation tool. J. Logic Program. 13(4), 349–366 (1992)
Pivotal Software Inc. Spring Framework. https://projects.spring.io/spring-framework
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of Principles of Programming Languages (POPL 2001), pp. 81–92. ACM (2001)
MITRE/SANS. Top 25 Most Dangerous Software Errors. http://cwe.mitre.org/top25. September 2011
Nikolić, Ð., Spoto, F.: Definite expression aliasing analysis for Java bytecode. In: Roychoudhury, A., D’Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 74–89. Springer, Heidelberg (2012)
Nikolić, Ð., Spoto, F.: Reachability analysis of program variables. ACM Trans. Program. Lang. Syst. (TOPLAS) 35(4), 14 (2013)
Palsberg, J., Schwartzbach, M.I.: Object-oriented type inference. In: Proceedings of Object-Oriented Programming, Systems, Languages & Applications (OOPSLA 1991). ACM SIGPLAN Notices, vol. 26(11), pp. 146–161. ACM, November 1991
Payet, É., Spoto, F.: Magic-sets transformation for the analysis of Java bytecode. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 452–467. Springer, Heidelberg (2007)
Payet, É., Spoto, F.: Static analysis of android programs. Inf. Softw. Technol. 54(11), 1192–1201 (2012)
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Raychev, V., Bielik, P., Vechev, M.T., Krause, A.: Learning programs from noisy data. In: Proceedings of Principles of Programming Languages (POPL 2016), St. Petersburg, FL, USA, pp. 761–774. ACM (2016)
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, pp. 95–110. Springer, Heidelberg (2006)
Secci, S., Spoto, F.: Pair-sharing analysis of object-oriented programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 320–335. Springer, Heidelberg (2005)
Spoto, F.: Precise null-pointer analysis. Softw. Syst. Model. 10(2), 219–252 (2011)
Spoto, F., Ernst, M.D.: Inference of field initialization. In: Proceedings of Software Engineering (ICSE 2011), Waikiki, Honolulu, USA, pp. 231–240. ACM (2011)
Spoto, F., Jensen, T.P.: Class analyses as abstract interpretations of trace semantics. ACM Trans. Program. Lang. Syst. (TOPLAS) 25(5), 578–630 (2003)
Spoto, F., Mesnard, F., Payet, É.: A termination analyzer for Java bytecode based on path-length. ACM Trans. Program. Lang. Syst. (TOPLAS) 32(3), 1–70 (2010)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag GmbH Germany
About this paper
Cite this paper
Spoto, F. (2016). The Julia Static Analyzer for Java. In: Rival, X. (eds) Static Analysis. SAS 2016. Lecture Notes in Computer Science(), vol 9837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53413-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-662-53413-7_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-53412-0
Online ISBN: 978-3-662-53413-7
eBook Packages: Computer ScienceComputer Science (R0)