×

zbMATH — the first resource for mathematics

Sawja: static analysis workshop for Java. (English) Zbl 1308.68028
Beckert, Bernhard (ed.) et al., Formal verification of object-oriented software. International conference, FoVeOOS 2010, Paris, France, June 28–30, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-18069-9/pbk). Lecture Notes in Computer Science 6528, 92-106 (2011).
Summary: Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when developing a full-fledged analyzer for a realistic language such as Java. Efficiency and precision of such a tool rely partly on low level components which only depend on the syntactic structure of the language and therefore should not be redesigned for each implementation of a new static analysis. This paper describes the Sawja library: a static analysis workshop fully compliant with Java 6 which provides OCaml modules for efficiently manipulating Java bytecode programs. We present the main features of the library, including i) efficient functional data-structures for representing a program with implicit sharing and lazy parsing, ii) an intermediate stack-less representation, and iii) fast computation and manipulation of complete programs. We provide experimental evaluations of the different features with respect to time, memory and precision.
For the entire collection see [Zbl 1204.68003].

MSC:
68N15 Theory of programming languages
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bacon, D.F., Sweeney, P.F.: Fast static analysis of C++ virtual function calls. In: Proc. of OOPSLA 1996, pp. 324–341 (1996) · doi:10.1145/236337.236371
[2] Bicolano - web home, http://mobius.inria.fr/bicolano
[3] Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proc. of PLDI 2003, San Diego, California, USA, June 7–14, pp. 196–207. ACM Press, New York (2003) · Zbl 1026.68514
[4] Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. SIGPLAN Not. 44(10), 243–262 (2009) · doi:10.1145/1639949.1640108
[5] Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Survey 24(3), 293–318 (1992) · doi:10.1145/136035.136043
[6] Burke, M.G., Choi, J., Fink, S., Grove, D., Hind, M., Sarkar, V., Serrano, M.J., Sreedhar, V.C., Srinivasan, H., Whaley, J.: The Jalapeño dynamic optimizing compiler for Java. In: Proc. of JAVA 1999, pp. 129–141. ACM, New York (1999)
[7] Clerc, X.: Barista, http://barista.x9c.fr/
[8] The Coq Proof Assistant, http://coq.inria.fr/ · Zbl 06496834
[9] Dean, J., Grove, D., Chambers, C.: Optimization of object-oriented programs using static class hierarchy analysis. In: Olthoff, W. (ed.) ECOOP 1995. LNCS, vol. 952, pp. 77–101. Springer, Heidelberg (1995) · Zbl 05761510 · doi:10.1007/3-540-49538-X_5
[10] Demange, D., Jensen, T., Pichardie, D.: A provably correct stackless intermediate representation for Java bytecode. Research Report 7021, INRIA (2009), http://www.irisa.fr/celtique/ext/bir/rr7021.pdf
[11] Ershov, A.P.: On programming of arithmetic operations. Commun. ACM 1(8), 3–6 (1958) · Zbl 0086.33203 · doi:10.1145/368892.368907
[12] Grove, D., Chambers, C.: A framework for call graph construction algorithms. Toplas 23(6), 685–746 (2001) · Zbl 05459271 · doi:10.1145/506315.506316
[13] Hubert, L.: A Non-Null annotation inferencer for Java bytecode. In: Proc. of PASTE 2008, pp. 36–42. ACM, New York (November 2008)
[14] Hubert, L., Jensen, T., Monfort, V., Pichardie, D.: Enforcing secure object initialization in java. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 101–115. Springer, Heidelberg (2010) · Zbl 05788998 · doi:10.1007/978-3-642-15497-3_7
[15] IBM: The T.J. Watson Libraries for Analysis (Wala), http://wala.sourceforge.net
[16] Jensen, T., Pichardie, D.: Secure the clones: Static enforcement of policies for secure object copying. Technical report, INRIA (June 2010); Presented at OWASP (2010) · Zbl 1326.68098
[17] Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system, Inria (May 2007), http://caml.inria.fr/ocaml/
[18] Lhoták, O., Hendren, L.: Scaling java points-to analysis using SPARK. In: Wang, H. (ed.) CC 2003. LNCS, vol. 2622, pp. 153–169. Springer, Heidelberg (2003) · Zbl 1032.68905 · doi:10.1007/3-540-36579-6_12
[19] Lhoták, O., Hendren, L.: Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation. ACM Trans. Softw. Eng. Methodol. 18(1) (2008) · Zbl 05517472 · doi:10.1145/1391984.1391987
[20] Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Prentice Hall PTR, Englewood Cliffs (1999)
[21] Livshits, V.B., Whaley, J., Lam, M.S.: Reflection analysis for java. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 139–160. Springer, Heidelberg (2005) · Zbl 1159.68375 · doi:10.1007/11575467_11
[22] Meyer, J., Downing, T.: Java Virtual Machine. O’Reilly Associates, Sebastopol (1997), http://jasmin.sourceforge.net · Zbl 0893.68018
[23] Morrison, D.R.: PATRICIA – Practical algorithm to retrieve information coded in alphanumeric. J. ACM 15(4) (1968) · doi:10.1145/321479.321481
[24] Pagano, B., Andrieu, O., Moniot, T., Canou, B., Chailloux, E., Wang, P., Manoury, P., Colaço, J.L.: Experience report: using Objective Caml to develop safety-critical embedded tools in a certification framework. In: Proc. of ICFP, pp. 215–220. ACM, New York (2009) · Zbl 06383956 · doi:10.1145/1596550.1596582
[25] Rose, E.: Lightweight bytecode verification. J. Autom. Reason. 31(3-4), 303–334 (2003) · Zbl 1069.68542 · doi:10.1023/B:JARS.0000021015.15794.82
[26] Spoto, F.: Julia: A generic static analyser for the Java bytecode. In: Proc. of the Workshop FTfJP (2005)
[27] Stata, R., Abadi, M.: A type system for Java bytecode subroutines. In: Proc. of POPL 1998, pp. 149–160. ACM Press, New York (1998)
[28] Tip, F., Palsberg, J.: Scalable propagation-based call graph construction algorithms. In: Proc. of OOPSLA 2000, pp. 281–293. ACM Press, New York (October 2000)
[29] Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - A Java bytecode optimization framework. In: Proc. of CASCON 1999 (1999)
[30] Whaley, J.: Dynamic optimization through the use of automatic runtime specialization. Master’s thesis, Massachusetts Institute of Technology (May 1999)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.