{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:07:33Z","timestamp":1751983653760},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657033"},{"type":"electronic","value":"9783540490593"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49059-0_7","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T21:56:57Z","timestamp":1194991017000},"page":"89-103","source":"Crossref","is-referenced-by-count":34,"title":["Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Cornelia","family":"Pusch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,3,12]]},"reference":[{"key":"7_CR1","unstructured":"Peter Berstelsen. Semantics of Java Byte Code.. http:\/\/www.dina.kvl.dk\/~pmb\/ , August 1997."},{"key":"7_CR2","unstructured":"Richard M. Cohen. The defensive Java Virtual Machine Specification. Technical report, Computational Logic Inc., 1997. Draft version."},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Stephen N. Freund and John C. Mitchell. A Type System for Object Initialization in the Java Bytecode Language. In ACM Conf. on Object-Oriented Programming: Systems, Languages and Applications, 1998.","DOI":"10.1145\/286936.286972"},{"key":"7_CR4","unstructured":"James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996."},{"key":"7_CR5","series-title":"Technical report","volume-title":"A Specification of Java Loading and Bytecode Verification","author":"A. Goldberg","year":"1997","unstructured":"A. Goldberg. A Specification of Java Loading and Bytecode Verification. Technical report, Kestrel Institute, Palo Alto, CA, 1997."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Pieter Hartel, Michael Butler, and Moshe Levy. The Operational Semantics of a Java Secure Processor. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes in Comp. Sci. Springer-Verlag, 1998.","DOI":"10.1007\/3-540-48737-9_9"},{"key":"7_CR7","unstructured":"The Isabelle library. http:\/\/www.in.tum.de\/~isabelle\/library\/ ."},{"key":"7_CR8","unstructured":"Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996."},{"key":"7_CR9","unstructured":"Tobias Nipkow, David von Oheimb, and Cornelia Pusch. Project Bali. http:\/\/www.in.tum.de\/~isabelle\/bali\/ ."},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"David von Oheimb and Tobias Nipkow. Machine-checking the Java specification: Proving type-safety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes in Comp. Sci. Springer-Verlag, 1998.","DOI":"10.1007\/3-540-48737-9_4"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"7_CR12","unstructured":"Cornelia Pusch. Formalizing the Java Virtual Machine in Isabelle. Technical Report TUM-I9816, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 1998. Available at http:\/\/www.in.tum.de\/~pusch\/ ."},{"key":"7_CR13","unstructured":"Zhenyu Qian. A formal specification of Java Virtual Machine instructions. Technical report, 1997. Dept. of Comp. Sci., University of Bremen."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Zhenyu Qian. A Formal Specification of Java Virtual Machine instructions for Objects, Methods and Subroutines. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes in Comp. Sci. Springer-Verlag, 1998.","DOI":"10.1007\/3-540-48737-9_8"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Raymie Stata and Mart\u00edn Abadi. A type system for Java bytecode subroutines. In Proc. 25th ACM Symp. Principles of Programming Languages. ACM Press, 1998. To appear.","DOI":"10.1145\/268946.268959"},{"key":"7_CR16","unstructured":"Types forum. http:\/\/www.cs.indiana.edu\/hyplan\/pierce\/types\/ ."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49059-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T11:00:29Z","timestamp":1556967629000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49059-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657033","9783540490593"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-49059-0_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}