{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:50Z","timestamp":1749124070711},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426103"},{"type":"electronic","value":"9783540454182"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1007\/3-540-45418-7_13","type":"book-chapter","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T17:08:09Z","timestamp":1180890489000},"page":"150-164","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["On-Card Bytecode Verification for Java Card"],"prefix":"10.1007","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,9,11]]},"reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1145\/177492.177575","volume":"16","author":"P. Briggs","year":"1994","unstructured":"P. Briggs, K. D. Cooper, and L. Torczon. Improvements to graph coloring register allocation. ACM Trans. Prog. Lang. Syst., 16(3):428\u2013455, 1994.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"13_CR2","unstructured":"P. Brisset. Vers un v\u00e9rifieur de bytecode Java certifi\u00e9. Seminar given at \u00c9cole Normale Sup\u00e9rieure, Paris, Oct 2nd 1998."},{"issue":"6","key":"13_CR3","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1145\/872726.806984","volume":"17","author":"G. J. Chaitin","year":"1982","unstructured":"G. J. Chaitin. Register allocation and spilling via graph coloring. SIGPLAN Notices, 17(6):98\u2013105, 1982.","journal-title":"SIGPLAN Notices"},{"key":"13_CR4","unstructured":"Z. Chen. Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide. The Java Series. Addison-Wesley, 2000."},{"key":"13_CR5","unstructured":"R. Cohen. The defensive Java virtual machine specification. Technical report, Computational Logic Inc., 1997."},{"issue":"6","key":"13_CR6","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1145\/330643.330646","volume":"21","author":"S. N. Freund","year":"1999","unstructured":"S. N. Freund and J. C. Mitchell. A type system for object initialization in the Java bytecode language. ACM Trans. Prog. Lang. Syst., 21(6):1196\u20131250, 1999.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"13_CR7","unstructured":"L. Gong. Inside Java 2 platform security: architecture, API design, and implementation. The Java Series. Addison-Wesley, 1999."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"J. A. Gosling. Java intermediate bytecodes. In Proc. ACM SIGPLAN Workshop on Intermediate Representations, pages 111\u2013118. ACM, 1995.","DOI":"10.1145\/202530.202541"},{"key":"13_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/3-540-48166-4_29","volume-title":"Software Engineering-ESEC\/FSE\u2019 99","author":"G. Grimaud","year":"1999","unstructured":"G. Grimaud, J.-L. Lanet, and J.-J. Vandewalle. FACADE-a typed intermediate language dedicated to smart cards. In Software Engineering-ESEC\/FSE\u2019 99, volume 1687 of LNCS, pages 476\u2013493. Springer-Verlag, 1999."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"T. Lindholm and F. Yellin. The Java Virtual Machine Specification. The Java Series. Addison-Wesley, 1999. Second edition.","DOI":"10.1007\/978-3-642-95851-9_5"},{"key":"13_CR11","unstructured":"G. McGraw and E. Felten. Securing Java. John Wiley & Sons, 1999."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"G. C. Necula. Proof-carrying code. In POPL\u201997, pages 106\u2013119. ACM Press, 1997.","DOI":"10.1145\/263699.263712"},{"key":"13_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-45315-6_23","volume-title":"Foundations of Software Science and Computation Structures (FOSSACS\u201901)","author":"T. Nipkow","year":"2001","unstructured":"T. Nipkow. Verified bytecode verifiers. In Foundations of Software Science and Computation Structures (FOSSACS\u201901), volume 2030 of LNCS, pages 364\u2013378. Springer-Verlag, 2001."},{"key":"13_CR14","unstructured":"J. Posegga and H. Vogt. Java bytecode verification using model checking. In OOPSLA Workshop Fundamental Underpinnings of Java, 1998."},{"key":"13_CR15","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":"C. Pusch. Proving the soundness of a Java bytecode verifier specification in Isabelle\/HOL. In W. R. Cleaveland, editor, TACAS\u201999, volume 1579 of LNCS, pages 89\u2013103. Springer-Verlag, 1999."},{"key":"13_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Formal syntax and semantics of Java","author":"Z. Qian","year":"1998","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. Springer-Verlag, 1998."},{"issue":"4","key":"13_CR17","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. Prog. Lang. Syst., 22(4):638\u2013672, 2000.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"13_CR18","unstructured":"E. Rose and K. Rose. Lightweight bytecode verification. In OOPSLA Workshop Fundamental Underpinnings of Java, 1998."},{"issue":"1","key":"13_CR19","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/314602.314606","volume":"21","author":"R. Stata","year":"1999","unstructured":"R. Stata and M. Abadi. A type system for Java bytecode subroutines. ACM Trans. Prog. Lang. Syst., 21(1):90\u2013137, 1999.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"13_CR20","unstructured":"Sun Microsystems. Java 2 platform micro edition technology for creating mobile devices. White paper, 2000."},{"key":"13_CR21","unstructured":"Sun Microsystems. Java Card 2.1.1 runtime environment specification, 2000."},{"key":"13_CR22","unstructured":"Sun Microsystems. Java Card 2.1.1 virtual machine specification, 2000."},{"key":"13_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Mobile Agents and Security","year":"1998","unstructured":"G. Vigna, editor. Mobile Agents and Security. Number 1419 in Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"13_CR24","unstructured":"F. Yellin. Low level security in Java. In Proc. 4th World Wide Web Conference, pages 369\u2013379. O\u2019Reilly, 1995."}],"container-title":["Lecture Notes in Computer Science","Smart Card Programming and Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45418-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:39:36Z","timestamp":1558258776000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45418-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426103","9783540454182"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45418-7_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"11 September 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}