{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T15:37:10Z","timestamp":1770219430885,"version":"3.49.0"},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2008,7,1]],"date-time":"2008-07-01T00:00:00Z","timestamp":1214870400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-01-1-0854"],"award-info":[{"award-number":["N00014-01-1-0854"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["TC-0209163ITR-0205712"],"award-info":[{"award-number":["TC-0209163ITR-0205712"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:p>Java Virtual Machines (JVMs) traditionally perform bytecode verification by way of an iterative dataflow analysis. Bytecode verification is necessary to ensure type safety because temporary variables in the JVM are not statically typed. We present an alternative verification mechanism that transforms JVM bytecode into Static Single Assignment Form (SSA) and thereby propagates definitions directly to uses. Type checking at control flow merge points can then be performed in a single pass.<\/jats:p>\n          <jats:p>Our prototype implementation of the new algorithm is faster than the standard JVM bytecode verifier. It has the additional benefit of generating SSA as a side effect, which may be immediately useful for a subsequent dynamic compilation stage.<\/jats:p>","DOI":"10.1145\/1377492.1377496","type":"journal-article","created":{"date-parts":[[2008,8,5]],"date-time":"2008-08-05T13:35:10Z","timestamp":1217943310000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Java bytecode verification via static single assignment form"],"prefix":"10.1145","volume":"30","author":[{"given":"Andreas","family":"Gal","sequence":"first","affiliation":[{"name":"University of California, Irvine"}]},{"given":"Christian W.","family":"Probst","sequence":"additional","affiliation":[{"name":"Technical University of Denmark, Kongens Lyngby"}]},{"given":"Michael","family":"Franz","sequence":"additional","affiliation":[{"name":"University of California, Irvine"}]}],"member":"320","published-online":{"date-parts":[[2008,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378825"},{"key":"e_1_2_1_2_1","unstructured":"Davey B. A. and Priestley H. A. 1990. Introduction to Lattices and Order. Cambridge University Press.  Davey B. A. and Priestley H. A. 1990. Introduction to Lattices and Order. Cambridge University Press."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200003)30:3%3C199::AID-SPE296%3E3.0.CO;2-2"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the Formal Underpinnings of Java Workshop at OOPSLA.","author":"Freund S. N.","year":"1998","unstructured":"Freund , S. N. 1998 . The costs and benefits of java bytecode subroutines . In Proceedings of the Formal Underpinnings of Java Workshop at OOPSLA. Freund, S. N. 1998. The costs and benefits of java bytecode subroutines. In Proceedings of the Formal Underpinnings of Java Workshop at OOPSLA."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320397"},{"key":"e_1_2_1_6_1","unstructured":"Freund S. N. and Mitchell J. C. 1999b. Specification and verification of Java bytecode subroutines and exceptions. Tech. rep. CS-TN-99-91 Stanford University.  Freund S. N. and Mitchell J. C. 1999b. Specification and verification of Java bytecode subroutines and exceptions. Tech. rep. CS-TN-99-91 Stanford University."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025011624925"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 4th International Workshop on Compiler Optimization Meets Compiler Verification (COCV'05)","author":"Gal A.","unstructured":"Gal , A. , Probst , C. W. , and Franz , M . 2005. Structural encoding of static single assignment form . In Proceedings of the 4th International Workshop on Compiler Optimization Meets Compiler Verification (COCV'05) . Elsevier Science Publishers, Amsterdam, The Netherlands. Gal, A., Probst, C. W., and Franz, M. 2005. Structural encoding of static single assignment form. In Proceedings of the 4th International Workshop on Compiler Optimization Meets Compiler Verification (COCV'05). Elsevier Science Publishers, Amsterdam, The Netherlands."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 5th World Conference on Systemics, Cybernetics, and Informatics Workshop on Intermediate Representation Engineering for the Java Virtual Machine.","author":"League C.","unstructured":"League , C. , Trifonov , V. , and Shao , Z . 2001. Functional Java Bytecode . In Proceedings of the 5th World Conference on Systemics, Cybernetics, and Informatics Workshop on Intermediate Representation Engineering for the Java Virtual Machine. League, C., Trifonov, V., and Shao, Z. 2001. Functional Java Bytecode. In Proceedings of the 5th World Conference on Systemics, Cybernetics, and Informatics Workshop on Intermediate Representation Engineering for the Java Virtual Machine."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025055424017"},{"key":"e_1_2_1_11_1","unstructured":"Lindholm T. and Yellin F. 1996. The Java Virtual Machine Specification. Addison Wesley Reading MA.   Lindholm T. and Yellin F. 1996. The Java Virtual Machine Specification. Addison Wesley Reading MA."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of Eurocast'01 Formal Methods and Tools for Computer Science, R. Moreno-D\u00edaz and A. Quesada-Arencibia, Eds. 232--234","author":"St\u00e4rk R.","unstructured":"St\u00e4rk R. and Schmid , J . 2001. Java bytecode verification is not possible (extended abstract) . In Proceedings of Eurocast'01 Formal Methods and Tools for Computer Science, R. Moreno-D\u00edaz and A. Quesada-Arencibia, Eds. 232--234 . St\u00e4rk R. and Schmid, J. 2001. Java bytecode verification is not possible (extended abstract). In Proceedings of Eurocast'01 Formal Methods and Tools for Computer Science, R. Moreno-D\u00edaz and A. Quesada-Arencibia, Eds. 232--234."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"St\u00e4rk R. Schmid J. and B\u00f6rger E. 2001. Java and the Java Virtual Machine: Definition Verification Validation. Springer-Verlag Berlin Germany.   St\u00e4rk R. Schmid J. and B\u00f6rger E. 2001. Java and the Java Virtual Machine: Definition Verification Validation. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-3-642-59495-3"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/314602.314606"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1377492.1377496","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1377492.1377496","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:57:55Z","timestamp":1750255075000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1377492.1377496"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7]]},"references-count":14,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["10.1145\/1377492.1377496"],"URL":"https:\/\/doi.org\/10.1145\/1377492.1377496","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,7]]},"assertion":[{"value":"2006-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}