{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:43Z","timestamp":1749124063358,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540650041"},{"type":"electronic","value":"9783540497844"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055863","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T16:50:09Z","timestamp":1154019009000},"page":"175-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Byte code verification for Java smart cards based on model checking"],"prefix":"10.1007","author":[{"given":"Joachim","family":"Posegga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Vogt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,28]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger and W. Schulte. Programmer Friendly Modular Definition of the Semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS. Springer, 1998.","DOI":"10.1007\/3-540-48737-9_10"},{"issue":"5","key":"12_CR2","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, D. Grumberg, and D. Long. Model Checking and Abstraction. ACM Trans. on Prog. Languages and Systems, 16(5):1512\u20131542, 1994.","journal-title":"ACM Trans. on Prog. Languages and Systems"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In A Decade of Concurrency \u2014 Reflections and Perspectives, volume 803 of Lecture Notes in Computer Science. Springer Verlag, 1995.","DOI":"10.1007\/3-540-58043-3_19"},{"key":"12_CR4","unstructured":"Richard M. Cohen. The Defensive Java Virtual Machine Specification Version, Alpha 1 Release. Technical report, Computational Logic, Inc; http:\/\/www.cri.com\/software\/djvm\/html-0.5\/djvm-report.html, 1996."},{"key":"12_CR5","volume-title":"Working Paper","author":"S. Drossopoulou","year":"1997","unstructured":"Sophia Drossopoulou and Susan Eisenbach. Proving the Soundness of the Java Type System. Working Paper, Imperial College, Dept. of Computing, London, UK, Feb. 1997."},{"key":"12_CR6","volume-title":"Java security: From HotJava to Netscape","author":"D. Dean","year":"1996","unstructured":"Drew Dean, Edward W. Felten, and Dan S. Wallach. Java security: From HotJava to Netscape. In IEEE Symposium on Security and Privacy, Oakland, CA, May 1996. IEEE. http:\/\/www.cs.princeton.edu\/sip\/pub\/secure96.html."},{"issue":"3","key":"12_CR7","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. A. Emerson","year":"1982","unstructured":"E. Allen Emerson and Edmund M. Clarke. Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming, 2(3):241\u2013266, December 1982.","journal-title":"Science of Computer Programming"},{"key":"12_CR8","unstructured":"J. Feigenbaum and P. Lee. Trust Management and Proof-Carrying Code for Mobile Code Security. In DARPA Workshop on Foundations of Mobile Code Security, Monterey, CA, 26\u201328 March 1997."},{"key":"12_CR9","unstructured":"J. Gosling and G. Steele. The Java Language Specification. Addison-Wesley, 1996."},{"issue":"1","key":"12_CR10","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s002870050087","volume":"21","author":"M. Kaiserswerth","year":"1998","unstructured":"Matthias Kaiserswerth and Joachim Posegga. Java Chipkarten. Informatik-Spektrum, 21(1):27\u201328, 1998.","journal-title":"Informatik-Spektrum"},{"key":"12_CR11","unstructured":"T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996."},{"key":"12_CR12","volume-title":"Technical Report CMU-CS-96-165","author":"G. Necula","year":"1996","unstructured":"G. Necula and P. Lee. Proof-Carrying Code. Technical Report CMU-CS-96-165, Carnegie Mellon University, School of Computer Science, Pittsburg, PA, September 1996."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow and David von Oheimb. Javalight is Type-Safe \u2014 Definitely. In Proc. 25th ACM Symp. Principles of Programming Languages. ACM Press, 1998.","DOI":"10.1145\/268946.268960"},{"issue":"1","key":"12_CR14","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/s002870050085","volume":"21","author":"J. Posegga","year":"1998","unstructured":"Joachim Posegga. Die Sicherheitsaspekte von Java. Informatik-Spektrum, 21(1):16\u201322, 1998.","journal-title":"Informatik-Spektrum"},{"key":"12_CR15","unstructured":"Z. Qian. A Formal Specification of Java Virtual Machine Instructions. (unpublished manuscript), 1997."},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Raymie Stata and Martin Abadi. A Type System for Java Bytecode Subroutines. In Proc. 25th ACM Symp. Principles of Programming Languages. ACM Press, 1998.","DOI":"10.1145\/268946.268959"},{"key":"12_CR17","unstructured":"Schlumberger, Inc. Cyberflex 2.0 Multi 8K Programmer\u2019s Guide. http:\/\/www.cyberflex.austin.et.slb.com\/cyberflex\/docs\/docs-page3.htm, 1997."},{"key":"12_CR18","unstructured":"Emin G\u00fcn Sirer, Arthur J. Gregory, and Brian N. Bershad. Kimera: A Java System Architecture. http:\/\/kimera.cs.washington.edu\/, 1998."},{"key":"12_CR19","unstructured":"Sun Microsystems, Inc. Java Card 2.0 Application Programming Interfaces, Revision 1.0 Final. http:\/\/java.sun.com:80\/products\/javacard\/, October 13 1997."},{"key":"12_CR20","unstructured":"Sun Microsystems, Inc. Java Card 2.0 Language Subset and Virtual Machine Specification, Revision 1.0 Final. http:\/\/java.sun.com80\/products\/javacard\/, October 13 1997."},{"key":"12_CR21","unstructured":"Don Syme. Proving Java Type Soundness. Technical report, University of Cambridge Computer Laboratory, 1997."},{"key":"12_CR22","unstructured":"Frank Yellin. Low Level Security in Java. In WWW4, 1995. http:\/\/www.w3.org\/pub\/Conferences\/WWW4\/Papers\/197\/40.html."}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2014 ESORICS 98"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055863","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T20:06:43Z","timestamp":1559506003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540650041","9783540497844"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0055863","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"28 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}