{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:07Z","timestamp":1749125167037},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418641"},{"type":"electronic","value":"9783540453154"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45315-6_23","type":"book-chapter","created":{"date-parts":[[2007,12,3]],"date-time":"2007-12-03T06:28:39Z","timestamp":1196663319000},"page":"347-363","source":"Crossref","is-referenced-by-count":31,"title":["Verified Bytecode Verifiers"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"23_CR1","unstructured":"Y. Bertot. A Coq formalization of a type checker for object initialization in the Java Virtula Machine. Technical Report RR-4047, INRIA, Nov. 2000."},{"key":"23_CR2","unstructured":"L. Casset and J. L. Lanet. A formal specification of the Java bytecode semantics using the B method. In ECOOP\u201999 Workshop Formal Techniques for Java Programs, 1999."},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/DISCEX.2000.821537","volume":"2","author":"A. Coglio","year":"2000","unstructured":"A. Coglio, A. Goldberg, and Z. Qian. Toward a provably-correct implementation of the JVM bytecode verifier. In Proc. DARPA Information Survivability Conference and Exposition (DISCEX\u201900), Vol. 2, pages 403\u2013410. IEEE Computer Society Press, 2000.","journal-title":"Proc. DARPA Information Survivability Conference and Exposition (DISCEX\u201900)"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"S. N. Freund and J. C. Mitchell. A type system for object initialization in the Java bytecode language. In ACM Conf. Object-Oriented Programming: Systems, Languages and Applications, 1998.","DOI":"10.1145\/286936.286972"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"S. N. Freund and J. C. Mitchell. A formal framework for the java bytecode language and verifier. In ACM Conf. Object-Oriented Programming: Systems, Languages and Applications, 1999.","DOI":"10.1145\/320384.320397"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"A. Goldberg. A specification of Java loading and bytecode verification. In Proc. 5th ACM Conf. Computer and Communications Security, 1998.","DOI":"10.1145\/288090.288104"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"M. Hagiya and A. Tozawa. On a new method for dataflow analysis of Java virtual machine subroutines. In G. Levi, editor, Static Analysis (SAS\u201998), volume 1503 of Lect. Notes in Comp. Sci., pages 17\u201332. Springer-Verlag, 1998.","DOI":"10.1007\/3-540-49727-7_2"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"G. A. Kildall. A unified approach to global program optimization. In Proc. ACM Symp. Principles of Programming Languages, pages 194\u2013206, 1973.","DOI":"10.1145\/512927.512945"},{"key":"23_CR9","unstructured":"T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996."},{"key":"23_CR10","unstructured":"S. S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997."},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"T. Nipkow and D. v. Oheimb. Javalight is type-safe \u2014 definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 161\u2013170, 1998.","DOI":"10.1145\/268946.268960"},{"key":"23_CR12","unstructured":"T. Nipkow, D. v. Oheimb, and C. Pusch. \u03bcJava: Embedding a programming language in a theorem prover. In F. Bauer and R. Steinbruggen, editors, Foundations of Secure Computation, pages 117\u2013144. IOS Press, 2000."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"C. Pusch. Proving the soundness of a Java bytecode verifier specification in Isabelle\/HOL. In W. Cleaveland, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), volume 1579 of Lect. Notes in Comp. Sci., pages 89\u2013103. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-49059-0_7"},{"key":"23_CR14","doi-asserted-by":"crossref","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 Lect. Notes in Comp. Sci., pages 271\u2013311. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48737-9_8"},{"key":"23_CR15","unstructured":"Z. Qian. Standard fixpoint iteration for Java bytecode verification. ACM Trans. Programming Languages and Systems, ?:?-?, 200? Accepted for publication."},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 149\u2013161. ACM Press,1998.","DOI":"10.1145\/268946.268959"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45315-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T13:10:04Z","timestamp":1557061804000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45315-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418641","9783540453154"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45315-6_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}