{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:45:55Z","timestamp":1725489955788},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540401612"},{"type":"electronic","value":"9783540448433"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44843-8_60","type":"book-chapter","created":{"date-parts":[[2007,8,15]],"date-time":"2007-08-15T07:42:01Z","timestamp":1187163721000},"page":"552-561","source":"Crossref","is-referenced-by-count":0,"title":["An Efficient Small Sized On-Card Verifier for Java Card"],"prefix":"10.1007","author":[{"given":"Jeung-Bo","family":"Cho","sequence":"first","affiliation":[]},{"given":"Min-Soo","family":"Jung","sequence":"additional","affiliation":[]},{"given":"Sung-Ik","family":"Jun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"key":"60_CR1","unstructured":"Z. Chen. Java Card Technology for Smart Cards. Addison Wesley, 2000"},{"key":"60_CR2","doi-asserted-by":"crossref","unstructured":"C. Colby, G. C. Necula, and P. Lee. A Proof-Carrying Code Architecture for Java. In Computer Aided Verification, 2000.","DOI":"10.1007\/10722167_44"},{"key":"60_CR3","doi-asserted-by":"crossref","unstructured":"X. Leroy. Java bytecode verification: an overview. In Computer Aided Verification, 2001.","DOI":"10.1007\/3-540-44585-4_26"},{"key":"60_CR4","doi-asserted-by":"crossref","unstructured":"X. Leroy. On-card bytecode verification for java card. In Esmart, 2001.","DOI":"10.1007\/3-540-45418-7_13"},{"key":"60_CR5","doi-asserted-by":"crossref","unstructured":"X. Leroy. Bytecode verification for Java smart card. Software Practice & Experience, 2002.","DOI":"10.1002\/spe.438"},{"key":"60_CR6","doi-asserted-by":"crossref","unstructured":"G. C. Necula and P. Lee. Proof-carrying code. In Proceedings of the 24 th ACM SIGPLAN-SICACT Symposium on Principles of Programming Languages (POPL\u2019 97), 1997.","DOI":"10.1145\/263699.263712"},{"key":"60_CR7","unstructured":"E. Rose and K.H. Rose. Lightweight bytecode verification. In Workshop of the Formal Underpinnings of the Java Paradigm, OOPSLA\u2019 98 1998."},{"key":"60_CR8","unstructured":"Sun Microsystem. Connected Limited Device Configuration and K Virtual Machine. http:\/\/java.sun.com\/products\/cldc\/ ."},{"key":"60_CR9","unstructured":"Trusted Logic. Formal methods, smart card, security. http:\/\/www.trustedlogic.com\/ ."},{"key":"60_CR10","unstructured":"Damien Deville. Building an \u201cimpossible\u201d verifier on a Java Card."},{"key":"60_CR11","unstructured":"Ludovic Casset. Formal Development of an Embedded Verifier for Java Card Byte Code."},{"key":"60_CR12","unstructured":"Sun Microsystem. Java Card 2.1.1 Virtual Machine Specification, 2000."},{"key":"60_CR13","doi-asserted-by":"crossref","unstructured":"B. Venners, Inside Java Virtual Machine, McGraw-Hill,1997.","DOI":"10.1016\/S1353-4858(97)83033-4"},{"key":"60_CR14","unstructured":"Sun Microsystems, http:\/\/java.sun.com\/ , Java Home Page."},{"key":"60_CR15","unstructured":"Java Card Forums, http:\/\/www.javacardforum.org Java Card Forum Home Page."},{"key":"60_CR16","unstructured":"Sun Microsystems. JavaCard 2.2 Development Kit User\u2019s guide specification, 2002"},{"key":"60_CR17","unstructured":"Sun Microsystems. JavaCard 2.2 Application Programming notes, 2002."},{"key":"60_CR18","unstructured":"Sun Microsystems. JavaCard 2.2 Off-Card Verifier, White paper,2002."},{"key":"60_CR19","unstructured":"Sun Microsystems. Java Virtual Machine Specs, 2002."},{"key":"60_CR20","unstructured":"Wook-Chul Hwang. A study on the optimization of the Java Card Virtual Machine based on smart card, 2001."},{"key":"60_CR21","unstructured":"Gong L. Inside Java 2 platform security: architecture, API design, and implementation. The Java Series. Addison-Wesley, 1999."},{"key":"60_CR22","doi-asserted-by":"crossref","unstructured":"Lars R. Clausen, Ulrik Pagh Schultz, Charles Consel, and Gilles Muller, \u201cJava Bytecode Compression for Low-End Embeded Systems\u201d, ACM Transactions on Programming Languages and Systems, Vol. 22, No. 3, 2000.","DOI":"10.1145\/353926.353933"},{"key":"60_CR23","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1002\/(SICI)1096-9128(199711)9:11<1031::AID-CPE354>3.0.CO;2-O","volume":"9","author":"L.R. Clausen","year":"1997","unstructured":"Clausen. L. R, \u201cA Java bytecode optimizer using side-effect analysis\u201d, Concurrency: Practice and Experience 9, pages 1031\u20131045, 1997.","journal-title":"Concurrency: Practice and Experience"},{"key":"60_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-49059-0_7","volume-title":"TACAS\u201999","author":"C. Pusch","year":"1999","unstructured":"Pusch C. Proving the soundness of a Java bytecode verifier specification in Isabelle\/HOL. In TACAS\u201999, Cleaveland WR (ed.), volume 1579 of LNCS, pages 89\u2013103. Springer-Verlag, 1999."},{"key":"60_CR25","unstructured":"Sun Microsystems. Java 2 platform micro edition technology for creating mobile devices. White paper, http:\/\/java.sun.com\/products\/cldc\/wp\/KVMwp.pdf , 2000."},{"key":"60_CR26","unstructured":"Jeung-Bo Cho. Design and implementation of On-Card Verifier for Java card based on smart card, 2002"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2014 ICCSA 2003"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44843-8_60","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T02:14:34Z","timestamp":1556763274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44843-8_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540401612","9783540448433"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-44843-8_60","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}