{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:47Z","timestamp":1749124067604},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_5","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"47-66","source":"Crossref","is-referenced-by-count":11,"title":["Verified Bytecode Model Checkers"],"prefix":"10.1007","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Friedrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marek","family":"Gawkowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-46017-9_6","volume-title":"9th International SPIN Workshop on Model Checking of Software","author":"D. Basin","year":"2002","unstructured":"D. Basin, S. Friedrich, M.J. Gawkowski, and J. Posegga. Bytecode Model Checking: An Experimental Analysis. In 9th International SPIN Workshop on Model Checking of Software, 2002, volume 2318 of LNCS, pages 42\u201359, Grenoble. Springer-Verlag, 2002."},{"key":"5_CR2","unstructured":"Y. Bertot. A Coq formalization of a type checker for object initialization in the Java Virtual Machine. Technical Report RR-4047, INRIA, Nov. 2000."},{"key":"5_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":"5_CR4","doi-asserted-by":"crossref","unstructured":"S. Freund and J. Mitchell. A type system for object initialisation in the Java byte-code language. In ACM Conf. Object-Oriented Programming: Systems, Languages and Applications, 1998.","DOI":"10.1145\/286936.286972"},{"key":"5_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":"5_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":"5_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-49727-7_2","volume-title":"Static Analysis (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. Static Analysis (SAS\u201998), volume 1503 of LNCS, pages 17\u201332. Springer-Verlag, 1998."},{"key":"5_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":"5_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-44585-4_26","volume-title":"CAV 2001","author":"X. Leroy","year":"2001","unstructured":"X. Leroy. Java Bytecode Verification: An Overview. In G. Berry, H. Comon, and A. Finkel, editors. CAV 2001, LNCS, pages 265\u2013285. Springer-Verlag, 2001."},{"key":"5_CR10","unstructured":"T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Verified Bytecode Verifiers. In Foundations of Software Science and Computation Structure (FOSSACS\u201901), pages 347\u2013363, Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45315-6_23"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"T. Nipkow and D. v. Oheimb. Javaligth is type-safe-definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 161\u2013170, 1998.","DOI":"10.1145\/268946.268960"},{"key":"5_CR13","unstructured":"T. Nipkow, D.v. Oheimb, and C. Pusch. \u03bcJava: Embedding a programming language in a theorem prover. In F. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation, pages 117\u2013144. IOS Press, 2000."},{"key":"5_CR14","unstructured":"J. Posegga and H. Vogt. Java bytecode verification using model checking. In Workshop Fundamental Under spinnings of Java, 1998."},{"key":"5_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-49059-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999)","author":"C. Pusch","year":"1999","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 1597 of LNCS, pages 89\u2013103. Springer-Verlag, 1999."},{"key":"5_CR16","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"},{"key":"5_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-48737-9_8","volume-title":"Formal Syntax and Semantics of Java","author":"Z. Qian","year":"1999","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, pages 271\u2013311. Springer-Verlag, 1999."},{"issue":"4","key":"5_CR18","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. Programming Languages and Systems, 22(4):638\u2013672, 2000.","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"5_CR19","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","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:38:17Z","timestamp":1556415497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}