{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:35Z","timestamp":1761611255940},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_26","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T14:39:50Z","timestamp":1265899190000},"page":"265-285","source":"Crossref","is-referenced-by-count":36,"title":["Java Bytecode Verification: An Overview"],"prefix":"10.1007","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In 26th symp. Principles of Progr. Lang, pages 147\u2013160. ACM Press, 1999.","DOI":"10.1145\/292540.292555"},{"key":"26_CR2","unstructured":"Y. Bertot. A Coq formalization of a type checker for object initialization in the Java virtual machine. Research report 4047, INRIA, 2000. Also published in the proceedings of CAV\u201901."},{"key":"26_CR3","unstructured":"P. Brisset. Vers un v\u00e9rifieur de bytecode Java certifi\u00e9. Seminar given at Ecole Normale Sup\u00e9rieure, Paris, October 2nd 1998."},{"key":"26_CR4","unstructured":"K. Brunnstein. Hostile ActiveX control demonstrated. RISKS Forum, 18(82), Feb. 1997."},{"key":"26_CR5","unstructured":"Z. Chen. Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide. The Java Series. Addison-Wesley, 2000."},{"key":"26_CR6","unstructured":"R. Cohen. The defensive Java virtual machine specification. Technical report, Computational Logic Inc., 1997."},{"key":"26_CR7","unstructured":"S. N. Freund and J. C. Mitchell. A type system for object initialization in the Java bytecode language. ACM Trans. Prog. Lang. Syst., 22(5), 2000."},{"key":"26_CR8","unstructured":"L. Gong. Inside Java 2 platform security: architecture, API design, and implementation. The Java Series. Addison-Wesley, 1999."},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"J. A. Gosling. Java intermediate bytecodes. In Proc. ACM SIGPLAN Workshop on Intermediate Representations, pages 111\u2013118. ACM, 1995.","DOI":"10.1145\/202529.202541"},{"key":"26_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/3-540-49727-7_2","volume-title":"SAS\u201998","author":"M. Hagiya","year":"1998","unstructured":"M. Hagiya and A. Tozawa. On a new method for dataflow analysis of Java virtual machine subroutines. In G. Levi, editor, SAS\u201998, volume 1503 of LNCS, pages 17\u201332. Springer-Verlag, 1998."},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In 25th symp. Principles of Progr. Lang, pages 365\u2013377. ACM Press, 1998.","DOI":"10.1145\/268946.268976"},{"key":"26_CR12","unstructured":"M. Huisman, B. Jacobs, and J. van den Berg. A case study in class library verification: Java\u2019s Vector class. Technical Report CSI-R0007, Computing Science Institute, University of Nijmegen, 2000."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"X. Leroy. On-card bytecode verification for Java Card. Submitted for publication, available from http:\/\/cristal.inria.fr\/~xleroy , 2001.","DOI":"10.1007\/3-540-45418-7_13"},{"key":"26_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-48749-2_7","volume-title":"Security properties of typed applets","author":"X. Leroy","year":"1999","unstructured":"X. Leroy and F. Rouaix. Security properties of typed applets, volume 1603 of LNCS, pages 147\u2013182. Springer-Verlag, 1999."},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"T. Lindholm and F. Yellin. The Java Virtual Machine Specification. The Java Series. Addison-Wesley, 1999. Second edition.","DOI":"10.1007\/978-3-642-95851-9_5"},{"key":"26_CR16","unstructured":"G. McGraw and E. Felten. Securing Java. John Wiley & Sons, 1999."},{"key":"26_CR17","unstructured":"S. S. Muchnick. Advanced compiler design and implementation. Morgan Kaufmann, 1997."},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"G. C. Necula. Proof-carrying code. In POPL\u201997, pages 106\u2013119. ACM Press, 1997.","DOI":"10.1145\/263699.263712"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"F. Nielson, H. R. Nielson, and C. Hankin. Principles of program analysis. Springer-Verlag, 1999.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Verified bytecode verifiers. In Foundations of Software Science and Computation Structures (FOSSACS\u201901). Springer-Verlag, 2001. To appear.","DOI":"10.1007\/3-540-45315-6_23"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"R. O'Callahan. A simple, comprehensive type system for Java bytecode subroutines. In POPL\u201999, pages 70\u201378. ACM Press, 1999.","DOI":"10.1145\/292540.292549"},{"key":"26_CR22","unstructured":"J. Posegga and H. Vogt. Java bytecode verification using model checking. In Workshop Fundamental Underpinnings of Java, 1998."},{"key":"26_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-45309-1_3","volume-title":"A systematic approach to static access control","author":"F. Pottier","year":"2001","unstructured":"F. Pottier, C. Skalka, and S. Smith. A systematic approach to static access control. In D. Sands, editor, Proceedings of the 10th European Symposium on Programming (ESOP\u201901), volume 2028 of LNCS, pages 30\u201345. Springer-Verlag, 2001."},{"key":"26_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-49059-0_7","volume-title":"TACAS\u201999","author":"C. Pusch","year":"1999","unstructured":"C. Pusch. Proving the soundness of a Java bytecode verifier specification in Isabelle\/HOL. In W. R. Cleaveland, editor, TACAS\u201999, volume 1579 of LNCS, pages 89\u2013103. Springer-Verlag, 1999."},{"key":"26_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Formal syntax and semantics of Java","author":"Z. Qian","year":"1998","unstructured":"Z. Qian. A formal specification of Java virtual machine instructions for objects, methods and subroutines. In J. Alves-Foss, editor, Formal syntax and semantics of Java, volume 1523 of LNCS. Springer-Verlag, 1998."},{"issue":"4","key":"26_CR26","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1145\/363911.363915","volume":"22","author":"Z. Qian","year":"2000","unstructured":"Z. Qian. Standard fixpoint iteration for Java bytecode verification. ACM Trans. Prog. Lang. Syst., 22(4):638\u2013672, 2000.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"26_CR27","unstructured":"E. Rose and K. Rose. Lightweight bytecode verification. In Workshop Fundamental Underpinnings of Java, 1998."},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"D. A. Schmidt. Data flow analysis is model checking of abstract interpretations. In POPL\u201998, pages 38\u201348. ACM Press, 1998.","DOI":"10.1145\/268946.268950"},{"issue":"1","key":"26_CR29","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/314602.314606","volume":"21","author":"R. Stata","year":"1999","unstructured":"R. Stata and M. Abadi. A type system for Java bytecode subroutines. ACM Trans. Prog. Lang. Syst., 21(1):90\u2013137, 1999.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"26_CR30","unstructured":"Sun Microsystems. Java 2 platform micro edition technology for creating mobile devices. White paper, http:\/\/java.sun.com\/products\/cldc\/wp\/KVMwp.pdf , 2000."},{"key":"26_CR31","unstructured":"Trusted Logic. Off-card bytecode verifier for Java Card. Distributed as part of Sun\u2019s Java Card Development Kit, 2001."},{"key":"26_CR32","series-title":"Lect Notes Comput Sci","volume-title":"Mobile Agents and Security","year":"1998","unstructured":"G. Vigna, editor. Mobile Agents and Security, volume 1419 of Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"26_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"A type-based approach to program security","author":"D. Volpano","year":"1997","unstructured":"D. Volpano and G. Smith. A type-based approach to program security. In Proceedings of TAPSOFT\u201997, Colloquium on Formal Approaches in Software Engineering, volume 1214 of LNCS, pages 607\u2013621. Springer-Verlag, 1997."},{"issue":"3","key":"26_CR34","first-page":"1","volume":"4","author":"D. Volpano","year":"1996","unstructured":"D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):1\u201321, 1996.","journal-title":"Journal of Computer Security"},{"key":"26_CR35","doi-asserted-by":"crossref","unstructured":"D. Walker. A type system for expressive security policies. In 27th symp. Principles of Progr. Lang, pages 254\u2013267. ACM Press, 2000.","DOI":"10.1145\/325694.325728"},{"key":"26_CR36","doi-asserted-by":"crossref","unstructured":"F. Yellin. Low level security in Java. In Proceedings of the Fourth International World Wide Web Conference, pages 369\u2013379. O'Reilly, 1995.","DOI":"10.1145\/3592626.3592656"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,23]],"date-time":"2024-03-23T19:34:23Z","timestamp":1711222463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}