{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:50Z","timestamp":1749182810692,"version":"3.41.0"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1023\/a:1025003423108","type":"journal-article","created":{"date-parts":[[2003,9,16]],"date-time":"2003-09-16T22:24:47Z","timestamp":1063751087000},"page":"323-361","source":"Crossref","is-referenced-by-count":3,"title":["Completeness of a Bytecode Verifier and a Certifying Java-to-JVM Compiler"],"prefix":"10.1007","volume":"30","author":[{"given":"Robert F.","family":"St\u00e4rk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Schmid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"5139607_CR1","first-page":"2","volume":"8","author":"E. B\u00f6rger","year":"2002","unstructured":"B\u00f6rger, E.: The origins and the development of the ASM method for high level system design and analysis, J. Universal Computer Science\n                  8(1) (2002), 2-74.","journal-title":"J. Universal Computer Science"},{"key":"5139607_CR2","unstructured":"Coglio, A.: Simple verification technique for complex Java bytecode subroutines, in Proc. 4th ECOOP Workshop on Formal Techniques for Java-like Programs, 2002."},{"key":"5139607_CR3","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P., Necula, G. C., Blau, F., Plesko, M. and Cline, K.: A certifying compiler for Java, in SIGPLAN Conference on Programming Language Design and Implementation, 2000, pp. 95-107.","DOI":"10.1145\/349299.349315"},{"issue":"6","key":"5139607_CR4","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1145\/330643.330646","volume":"21","author":"S. N. Freund","year":"1999","unstructured":"Freund, S. N. and Mitchell, J. C.: The type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems\n                  21(6) (1999), 1196-1250.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5139607_CR5","unstructured":"Gosling, J., Joy, B., Steele, G. and Bracha, G.: The Java\n                  (tm)\n                  Language Specification, 2nd edn, Addison-Wesley, 2000."},{"key":"5139607_CR6","unstructured":"Gurevich, Y.: Evolving algebras 1993: Lipari guide, in E. B\u00f6rger (ed.), Specification and Validation Methods, Oxford University Press, 1993, pp. 9-36."},{"key":"5139607_CR7","unstructured":"Haase, E.: JustIce: An implementation of a free class file verifier for Java, Technical Report, Institut f\u00fcr Informatik, Freie Universit\u00e4t Berlin, 2001, http:\/\/bcel.sourceforge.net\/ justice\/."},{"key":"5139607_CR8","unstructured":"Henrio, L. and Serpette, B.: A framework for bytecode verifiers: application to intra-procedural continuations, Technical Report, Inria Sophia-Antipolis, 2001."},{"key":"5139607_CR9","unstructured":"Klein, G. and Strecker, M.: Verified bytecode verification and type-certifying compilation, Technical Report, Technical University Munich, 2002."},{"key":"5139607_CR10","doi-asserted-by":"crossref","unstructured":"Leroy, X.: On-card bytecode verification for Java Card, in I. Attali and T. Jensen (eds.), Smart Card Programming and Security (E-smart 2001), 2001, pp. 150-164.","DOI":"10.1007\/3-540-45418-7_13"},{"key":"5139607_CR11","unstructured":"Lindholm, T. and Yellin, F.: The Java\n                  (tm)\n                  Virtual Machine Specification, 2nd edn, Addison-Wesley, 1999."},{"key":"5139607_CR12","doi-asserted-by":"crossref","unstructured":"O'Callahan, R.: A simple, comprehensive type system for Java bytecode subroutines, in Proc. 26th ACM Symposium on Principles of Programming Languages, 1998, pp. 70-78.","DOI":"10.1145\/292540.292549"},{"issue":"4","key":"5139607_CR13","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1145\/363911.363915","volume":"22","author":"Z. Qian","year":"2000","unstructured":"Qian, Z.: Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems\n                  22(4) (2000), 638-672.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5139607_CR14","unstructured":"Schmid, J.: Executing ASM specifications with AsmGofer, Web pages at http:\/\/www.tydo.de\/AsmGofer, 1999."},{"key":"5139607_CR15","unstructured":"Sirer, E., McDirmid, S. and Bershad, B.: Kimera: A Java system security architecture, http:\/\/kimera.cs.washington.edu\/, 1997."},{"key":"5139607_CR16","doi-asserted-by":"crossref","unstructured":"St\u00e4rk, R. F., Schmid, J. and B\u00f6rger, E.: Java and the Java Virtual Machine - Definition, Verification, Validation, Springer-Verlag, 2001.","DOI":"10.1007\/978-3-642-59495-3"},{"issue":"1","key":"5139607_CR17","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/314602.314606","volume":"21","author":"R. Stata","year":"1999","unstructured":"Stata, R. and Abadi, M.: A type system for Java bytecode subroutines, ACM Transactions on Programming Languages and Systems\n                  21(1) (1999), 90-137.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5139607_CR18","doi-asserted-by":"crossref","unstructured":"Strecker, M.: Investigating type-certifying compilation with Isabelle, in Proc. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2002.","DOI":"10.1007\/3-540-36078-6_27"},{"key":"5139607_CR19","unstructured":"Sun Microsystems: Connected, limited device configuration, Specification 1.0, Java 2 Platform Micro Edition, 2000."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025003423108.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1025003423108\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025003423108.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:32:28Z","timestamp":1749123148000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1025003423108"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":19,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["5139607"],"URL":"https:\/\/doi.org\/10.1023\/a:1025003423108","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}