Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Simulation and Invariance for Weak Consistency Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

The Julia Static Analyzer for Java

verfasst von : Fausto Spoto

Erschienen in: Static Analysis

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Quantitative Monitor Automata
Nächstes Kapitel Automated Verification of Linearization Policies
Fußnoten
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.
 
Literatur
1.
2.
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)CrossRef
3.
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)MathSciNetCrossRef
4.
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)MathSciNetCrossRefMATH
5.
Bryant, R.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)CrossRef
6.
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)CrossRef
7.
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)
8.
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)CrossRef
9.
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 CrossRef
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)
11.
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 CrossRef
12.
13.
14.
Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., Lea, D.: Java Concurrency in Practice. Addison Wesley, Reading (2006)
15.
Göransson, A.: Efficient Android Threading. O’Reilly Media, Sebastopol (2014)
16.
17.
Hermenegildo, M., Warren, D.S., Debray, S.K.: Global flow analysis as a practical compilation tool. J. Logic Program. 13(4), 349–366 (1992)CrossRef
18.
19.
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)
20.
21.
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)CrossRef
22.
Nikolić, Ð., Spoto, F.: Reachability analysis of program variables. ACM Trans. Program. Lang. Syst. (TOPLAS) 35(4), 14 (2013)MATH
23.
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
24.
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)CrossRef
25.
Payet, É., Spoto, F.: Static analysis of android programs. Inf. Softw. Technol. 54(11), 1192–1201 (2012)CrossRef
26.
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)CrossRef
27.
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)
28.
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)CrossRef
29.
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)CrossRef
30.
Spoto, F.: Precise null-pointer analysis. Softw. Syst. Model. 10(2), 219–252 (2011)CrossRef
31.
Spoto, F., Ernst, M.D.: Inference of field initialization. In: Proceedings of Software Engineering (ICSE 2011), Waikiki, Honolulu, USA, pp. 231–240. ACM (2011)
32.
Spoto, F., Jensen, T.P.: Class analyses as abstract interpretations of trace semantics. ACM Trans. Program. Lang. Syst. (TOPLAS) 25(5), 578–630 (2003)CrossRef
33.
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)CrossRef
34.
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)MATH
Metadaten
Titel
The Julia Static Analyzer for Java
verfasst von
Fausto Spoto
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
Buch
Static Analysis

Print ISBN: 978-3-662-53412-0

Electronic ISBN: 978-3-662-53413-7

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-662-53413-7_3