{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:24Z","timestamp":1761597024158},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_17","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"290-309","source":"Crossref","is-referenced-by-count":18,"title":["Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods"],"prefix":"10.1007","author":[{"given":"Ludovic","family":"Casset","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"J.R. Abrial, The B Book, Assigning Programs to Meanings, Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"17_CR2","unstructured":"Y. Bertot, A Coq formalization of a Type Checker for Object Initialization in the Java Virtual Machine, Research Report, INRIA Sophia Antipolis, 2001."},{"key":"17_CR3","unstructured":"L. Casset, J.-L. Lanet, A Formal Specification of the Java Byte Code Semantics using the B method, Proceedings of the ECOOP\u201999 workshop on Formal Techniques for Java Programs, Lisbon, June 1999."},{"key":"17_CR4","unstructured":"L. Casset, Formal Implementation of a Verification Algorithm Using the B Method, Proceedings of AFADL01, Nancy, France, June 2001"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/DISCEX.2000.821537","volume":"2","author":"A. Coglio","year":"2000","unstructured":"A. Coglio, Z. Qian and A. Goldberg, Towards a Provably-correct Implementation of the JVM Bytecode Verifier, In Proc. DARPA Information Survivability Conference and Exposition (DISCEX\u201900), Vol. 2, pages 403\u2013410, IEEE Computer Society, 2000.","journal-title":"Proc. DARPA Information Survivability Conference and Exposition (DISCEX\u201900)"},{"key":"17_CR6","unstructured":"G. Klein, T. Nipkow, Verified Lightweight Bytecode Verification, in ECOOP 2000 Workshop on Formal Techniques for Java Programs, pp. 35\u201342, Cannes, June 2000."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"X. Leroy, On-Card Byte Code Verification for Java Card, Proceedings of e-Smart, Cannes, France, September 2001.","DOI":"10.1007\/3-540-45418-7_13"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"X. Leroy, Bytecode Verification on Java smart Cards, to appear in Software Practice and Experience, 2002.","DOI":"10.1002\/spe.438"},{"key":"17_CR9","unstructured":"T. Lindholm, F. Yellin, The Java Virtual Machine Specification, Addison Wesley, 1996"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"G. Necula, P. Lee, Proof-Carrying Code, in 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106\u2013119, Paris, France, 1997. http:\/\/www-nt.cs.berkeley.edu\/home\/necula\/public_html\/popl97.ps.gz","DOI":"10.1145\/263699.263712"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"T. Nipkow, Verified Byte code Verifiers, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 2000. http:\/\/www.in.tum.de\/~nipkow","DOI":"10.1007\/3-540-45315-6_23"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"C. Pusch, Proving the Soundness of a Java Bytecode Verifier in Isabelle\/HOL, In OOPSLA\u201998 Workshop Formal Underpinnings of Java, 1998.","DOI":"10.1007\/3-540-49059-0_7"},{"key":"17_CR13","unstructured":"C. Pusch, T. Nipkow, D. von Oheimb, microJava: Embedding a Programming Language in a Theorem Prover. In Foundations of Secure Computation, IOS Press, 2000."},{"key":"17_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-48737-9_8","volume-title":"Formal Syntax and Semantics of Java","author":"Z. Qian","year":"1999","unstructured":"Z. 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 Lecture Notes in Computer Science, pages 271\u2013312. Springer, 1999."},{"key":"17_CR15","unstructured":"A. Requet, L. Casset, G. Grimaud, Application of the B Formal Method to the Proof of a Type Verification Algorithm, HASE 2000, Albuquerque, November 2000."},{"key":"17_CR16","unstructured":"E. Rose, K. H. Rose, Lightweight Bytecode Verification, in Formal Underpinnings of Java, OOPSLA\u201998 Workshop, Vancouver, Canada, October. 1998. http:\/\/www-dse.doc.ic.ac.uk\/~sue\/oopsla\/rose.f.ps"},{"key":"17_CR17","unstructured":"Java Card 2.1.1 Virtual Machine Specification, Sun Microsystem, 2000."},{"key":"17_CR18","unstructured":"Connected, Limited Device Configuration, Specification 1.0a, Java 2 Platform Micro Edition, Sun Microsystems, 2000."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T04:11:59Z","timestamp":1587528719000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}