{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:33:06Z","timestamp":1725492786059},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441441"},{"type":"electronic","value":"9783540457190"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45719-4_4","type":"book-chapter","created":{"date-parts":[[2007,10,9]],"date-time":"2007-10-09T14:55:00Z","timestamp":1191941700000},"page":"41-59","source":"Crossref","is-referenced-by-count":7,"title":["Tool-Assisted Specification and Verification of the JavaCard Platform"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Dufay","sequence":"additional","affiliation":[]},{"given":"Sim\u00e3o Melo","family":"de Sousa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"4_CR1","unstructured":"C. Alvarado and Q.-H. Nguyen. ELAN for equational reasoning in COQ. In J. Despeyroux, editor, Proceedings of LFM\u201900, 2000. Rapport Technique INRIA."},{"key":"4_CR2","unstructured":"D. Aspinall and A. Compagnoni. Heap-bound assembly language. Manuscript, 2001."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"4_CR4","unstructured":"A. Banerjee and D. A. Naumann. Secure Information Flow and Pointer Confinement in a Java-like Language. In Proceedings of CSFW\u201902. IEEE Computer Society Press, 2002."},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45699-6","volume-title":"Efficient Reasoning about Executable Specifications in Coq","author":"G. Barthe","year":"2002","unstructured":"G. Barthe and P. Courtieu. Efficient Reasoning about Executable Specifications in Coq. In C. Mu\u00f1oz and S. Tahar, editors, Proceedings of TPHOLs\u201902, volume 2xxx of Lecture Notes in Computer Science. Springer-Verlag, 2002. To appear."},{"key":"4_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-45418-7_2","volume-title":"Jakarta: a toolset to reason about the JavaCard platform","author":"G. Barthe","year":"2001","unstructured":"G. Barthe, G. Dufay, M. Huisman, and S. Melo de Sousa. Jakarta: a toolset to reason about the JavaCard platform. In I. Attali and T. Jensen, editors, Proceedings of e-SMART\u201901, volume 2140 of Lecture Notes in Computer Science, pages 2\u201318. Springer-Verlag, 2001."},{"key":"4_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/3-540-47813-2_3","volume-title":"A formal correspondence between offensive and defensive JavaCard virtual machines","author":"G. Barthe","year":"2002","unstructured":"G. Barthe, G. Dufay, L. Jakubiec, and S. Melo de Sousa. A formal correspondence between offensive and defensive JavaCard virtual machines. In A. Cortesi, editor, Proceedings of VMCAI\u201902, volume 2294 of Lecture Notes in Computer Science, pages 32\u201345. Springer-Verlag, 2002."},{"key":"4_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"A Formal Executable Semantics of the JavaCard Platform","author":"G. Barthe","year":"2001","unstructured":"G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, and S. Melo de Sousa. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP\u201901, volume 2028 of Lecture Notes in Computer Science, pages 302\u2013319. Springer-Verlag, 2001."},{"key":"4_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"The LOOP Compiler for Java and JML","author":"J. Berg van den","year":"2001","unstructured":"J. van den Berg and B. Jacobs. The LOOP Compiler for Java and JML. In T. Margaria and W. Yi, editors, Proceedings of TACAS\u201901, volume 2031 of Lecture Notes in Computer Science, pages 299\u2013312, 2001."},{"key":"4_CR10","unstructured":"M. Bezem, J. W. Klop, and R. de Vrijer, editors. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2002."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"P. Bieber, J. Cazin, V. Wiels, G. Zanon, P. Girard, and J.-L. Lanet. Electronic Purse Applet Certification. In S. Schneider and P. Ryan, editors, Proceedings of the Workshop on Secure Architectures and Information Flow, volume 32 of Electronic Notes in Theoretical Computer Science. Elsevier Publishing, 2000.","DOI":"10.1016\/S1571-0661(04)00092-1"},{"issue":"1","key":"4_CR12","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47\u201377, January 1997.","journal-title":"Journal of Symbolic Computation"},{"key":"4_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Development of an Embedded Verifier for JavaCard ByteCode using Formal Methods","author":"L. Casset","year":"2002","unstructured":"L. Casset. Development of an Embedded Verifier for JavaCard ByteCode using Formal Methods. In L.-H. Eriksson and P. A. Lindsay, editors, Proceedings of FME\u201902, Lecture Notes in Computer Science, 2002. To appear."},{"key":"4_CR14","unstructured":"L. Casset, L. Burdy, and A. Requet. Formal Development of an Embedded Verifier for JavaCard ByteCode. In Proceedings of DSN\u201902. IEEE Computer Society, 2002."},{"key":"4_CR15","unstructured":"L. Casset and J.-L. Lanet. A Formal Specification of the Java Byte Code Semantics using the B Method. In B. Jacobs, G. T. Leavens, P. M\u00fcller, and A. Poetzsch-Heffter, editors, Proceedings of Formal Techniques for Java Programs. Technical Report 251, Fernuniversit\u00e4t Hagen, 1999."},{"key":"4_CR16","unstructured":"Z. Chen. Java Card for Smart Cards: Architecture and Programmer\u2019s Guide. The Java Series. O\u2019Reilly, 2000."},{"key":"4_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/3-540-47993-7_10","volume-title":"A Simple and Practical Approach to Unit Testing: The JML and JUnit Way","author":"Y. Cheon","year":"2002","unstructured":"Y. Cheon and G. T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In B. Magnusson, editor, Proceedings of ECOOP\u201902, volume 2374 of Lecture Notes in Computer Science, pages 231\u2013255, 2002."},{"key":"4_CR18","unstructured":"Coq Development Team. The Coq Proof Assistant User\u2019s Guide. Version 7.2, January 2002."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"J. Corbett, M. Dwyer, J. Hatcli., C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting Finite-state Models from Java Source Code. In Proceedings of ICSE\u201900, pages 439\u2013448. ACM Press, 2000.","DOI":"10.1145\/337180.337234"},{"key":"4_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/3-540-48523-6_4","volume-title":"Type structure for low-level programming languages","author":"K. Crary","year":"1999","unstructured":"K. Crary and G. Morrisett. Type structure for low-level programming languages. In J. Wiedermann, P. van Emde Boas, and M. Nielsen, editors, Proceedings of ICALP\u201999, volume 1644 of Lecture Notes in Computer Science, pages 40\u201354, 1999."},{"issue":"6","key":"4_CR21","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. The type systemfor object initialization in the Java bytecode language. ACM Transactions on Programming Languages and Systems, 21(6):1196\u20131250, November 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR22","unstructured":"E. Gim\u00e9nez and O. Ly. Formal modeling and verification of the java card security architecture: from static checkings to embedded applet execution, 2002. Talk delivered at the Verificard\u201902 meeting, Marseille, 7\u20139 January 2002. Slides available at http:\/\/www-sop.inria.fr\/lemme\/verificard\/2002\/programme.html ."},{"issue":"4","key":"4_CR23","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/503112.503115","volume":"33","author":"P. Hartel","year":"2001","unstructured":"P. Hartel and L. Moreau. Formalizing the Safety of Java, the Java Virtual Machine and Java Card. ACM Computing Surveys, 33(4):517\u2013558, December 2001.","journal-title":"ACM Computing Surveys"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"G. Klein and T. Nipkow. Verified bytecode verifiers. Theoretical Computer Science, 2002. Submitted.","DOI":"10.1016\/S0304-3975(02)00869-1"},{"key":"4_CR25","unstructured":"Gemplus Research Labs. Java Card Common Criteria Certification Using Coq. Technical Report, 2001."},{"key":"4_CR26","series-title":"Lect Notes Comput Sci","first-page":"85","volume-title":"Formal Proof of Smart Card Applets Correctness","author":"J.-L. Lanet","year":"1998","unstructured":"J.-L. Lanet and A. Requet. Formal Proof of Smart Card Applets Correctness. In J.-J. Quisquater and B. Schneier, editors, Proceedings of CARDIS\u201998, volume 1820 of Lecture Notes in Computer Science, pages 85\u201397. Springer-Verlag, 1998."},{"key":"4_CR27","unstructured":"C. Laneve. A Type Systemfor JVM Threads. Theoretical Computer Science, 200x. To appear."},{"key":"4_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-44577-3_11","volume-title":"Informatics-10 Years Back, 10 Years Ahead","author":"K. R. M. Leino","year":"2001","unstructured":"K. R. M. Leino. Extended Static Checking: A Ten-Year Perspective. In R. Wilhelm, editor, Informatics-10 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 157\u2013175, 2001."},{"key":"4_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-44585-4_26","volume-title":"Java bytecode verification: an overview","author":"X. Leroy","year":"2001","unstructured":"X. Leroy. Java bytecode verification: an overview. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of CAV\u201901, volume 2102 of Lecture Notes in Computer Science, pages 265\u2013285. Springer-Verlag, 2001."},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"X. Leroy. On-card bytecode verification for Java card. In I. Attali and T. Jensen, editors, Proceedings e-Smart 2001, volume 2140, pages 150\u2013164. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45418-7_13"},{"key":"4_CR31","unstructured":"X. Leroy, D. Doligez, J. Garrigue, D. R\u00e9my, and J. Vouillon. The Objective Caml system, release 3.00, 2000."},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"G. C. Necula. Proof-carrying code. In Proceedings of POPL\u201997, pages 106\u2013119. ACM Press, 1997.","DOI":"10.1145\/263699.263712"},{"key":"4_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-45315-6_23","volume-title":"Verified Bytecode Verifiers","author":"T. Nipkow","year":"2001","unstructured":"T. Nipkow. Verified Bytecode Verifiers. In F. Honsell and M. Miculan, editors, Proceedings of FOSSACS\u201901, volume 2030 of Lecture Notes in Computer Science, pages 347\u2013363. Springer-Verlag, 2001."},{"key":"4_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002."},{"key":"4_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/BFb0055863","volume-title":"Byte Code Verification for Java Smart Cards Based on Model Checking","author":"J. Posegga","year":"1998","unstructured":"J. Posegga and H. Vogt. Byte Code Verification for Java Smart Cards Based on Model Checking. In J.-J. Quisquater, Y. Deswarte, C. Meadows, and D. Gollmann, editors, Proceedings of the ESORICS\u201998, volume 1485 of Lecture Notes in Computer Science, pages 175\u2013190. Springer-Verlag, 1998."},{"key":"4_CR36","unstructured":"A. Requet. A B Model for Ensuring Soundness of a Large Subset of the Java Card Virtual Machine. In S. Gnesi, I. Schieferdecker, and A. Rennoch, editors, Proceedings of FMICS\u201900, pages 29\u201346, 2000."},{"key":"4_CR37","unstructured":"N. Shankar, S. Owre, and J. M. Rushby. The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International, February 1993. Supplemented with the PVS2 Quick Reference Manual, 1997."},{"issue":"1","key":"4_CR38","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 systemfor Java bytecode subroutines. ACM Transactions on Programming Languages and Systems, 21(1):90\u2013137, January 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR39","unstructured":"Sun Microsystems, Inc., Palo Alto\/CA, USA. Java Card Platform Security, 2001. Technical White Paper."},{"key":"4_CR40","unstructured":"Sun Microsystems, Inc., Palo Alto\/CA, USA. Java Card 2.2 Application Programming Interface (API), 2002."},{"key":"4_CR41","unstructured":"Sun Microsystems, Inc., Palo Alto\/CA, USA. Java Card 2.2 Runtime Environment (JCRE) Specification, 2002."},{"key":"4_CR42","unstructured":"Sun Microsystems, Inc., Palo Alto\/CA, USA. Java Card 2.2 Virtual Machine Specification, 2002."},{"key":"4_CR43","unstructured":"K. N. Swadi and A. W. Appel. Typed machine language and its semantics. Manuscript, 2001."}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45719-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:09:20Z","timestamp":1556903360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45719-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441441","9783540457190"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/3-540-45719-4_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}