{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:42:38Z","timestamp":1725486158994},"publisher-location":"Berlin, Heidelberg","reference-count":34,"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_2","type":"book-chapter","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T21:08:09Z","timestamp":1180904889000},"page":"2-18","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Jakarta: A Toolset for Reasoning about JavaCard"],"prefix":"10.1007","author":[{"given":"G.","family":"Barthe","sequence":"first","affiliation":[]},{"given":"G.","family":"Dufay","sequence":"additional","affiliation":[]},{"given":"M.","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"S. Melo","family":"de Sousa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,9,11]]},"reference":[{"key":"2_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/3-540-63533-5_15","volume-title":"Proceedings of FME\u201997","author":"S. Agerholm","year":"1997","unstructured":"S. Agerholm and J. Frost. Towards an integrated CASE and theorem proving tool for VDM-SL. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, Proceedings of FME\u201997, volume 1313 of Lecture Notes in Computer Science, pages 278\u2013297. Springer-Verlag, 1997."},{"unstructured":"B. Barras, S. Boutin, C. Comes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, H. Laulh\u00e9re, P. Loiseleur, C. Mu\u00f1oz, C. Murthy, C. Parent-Vigouroux, C. Paulin-Mohring, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant User\u2019s Guide. Version 6.3.1, December 1999.","key":"2_CR2"},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Proceedings of ESOP\u201901","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."},{"unstructured":"S. Bensalem, V. Ganesh, Y. Lakhnech, C. Mu\u00f1oz, S. Owre, H. Rue\u00df, J. Rushby, V. Rusu, H. Sa\u00efdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. In Proceedings of NASA\u2019s Workshop on Formal Methods, 2000.","key":"2_CR4"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J. Bergstra","year":"1986","unstructured":"J. Bergstra and J. W. Klop. Conditional rewrite rules: confluence and termination. Journal of Computer and System Sciences, 32:323\u2013362, 1986.","journal-title":"Journal of Computer and System Sciences"},{"unstructured":"P. Bertelsen. Semantics of Java Byte Code. Master\u2019s thesis, Department of Computer Science, Royal Veterinary and Agricultural University of Copenhagen, 1997.","key":"2_CR6"},{"key":"2_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u201901","author":"Y. Bertot","year":"2001","unstructured":"Y. Bertot. Formalizing in Coq a type system for object initialization in the Java bytecode language. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of CAV\u201901, volume 2xxx of Lecture Notes in Computer Science. Springer-Verlag, 2001."},{"doi-asserted-by":"crossref","unstructured":"P. Bieber, J. Cazin, V. Wiels, G. Zanon, P. Girard, and J.-L. Lanet. Electronic purse applet certification: extended abstract. 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.","key":"2_CR8","DOI":"10.1016\/S1571-0661(04)00092-1"},{"key":"2_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/3-540-48737-9_10","volume-title":"Formal Syntax and Semantics of Java","author":"E. B\u00f6rger","year":"1999","unstructured":"E. B\u00f6rger and W. Schulte. A Programmer Friendly Modular Definition of the Semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 353\u2013404. Springer-Verlag, 1999."},{"doi-asserted-by":"crossref","unstructured":"P. Borras, D. Cl\u00e9ment, Th. Despeyroux, J. Incerpi, G. Kahn, B. Lang, and V. Pascual. Centaur: the system. In Proceedings of the ACM SIGSOFT\/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 14\u201324. ACM Press, 1988.","key":"2_CR10","DOI":"10.1145\/64137.65005"},{"issue":"5\u20136","key":"2_CR11","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"J. P. Bowen","year":"1995","unstructured":"J. P. Bowen and M. J. C. Gordon. A shallow embedding of Z in HOL. Information and Software Technology, 37(5\u20136):269\u2013276, 1995.","journal-title":"Information and Software Technology"},{"doi-asserted-by":"crossref","unstructured":"P. Cousot. Program analysis: The abstract interpretation perspective. ACM Computing Surveys, 28A(4es):165-es, December 1996.","key":"2_CR12","DOI":"10.1145\/242224.242433"},{"doi-asserted-by":"crossref","unstructured":"P. Cousot. Types as abstract interpretations, invited paper. In Proceedings of POPL\u201997, pages 316\u2013331. ACM Press, 1997.","key":"2_CR13","DOI":"10.1145\/263699.263744"},{"doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of POPL\u201977, pages 238\u2013252. ACM Press, 1977.","key":"2_CR14","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"A. van Deursen, J. Heering, and P. Klint, editors. Language Prototyping: an algebraic specification approach. AMAST Series in Computing. World Scientific, 1996.","key":"2_CR15","DOI":"10.1142\/3163"},{"key":"2_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-48737-9_2","volume-title":"Formal Syntax and Semantics of Java","author":"S. Drossopoulou","year":"1999","unstructured":"S. Drossopoulou and S. Eisenbach. Describing the semantics of Java and Proving Type Soundness. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 41\u201382. Springer-Verlag, 1999."},{"unstructured":"M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, and H. Zheng. Tool-supported program abstraction for finite-state verification. In Proceedings of ICSE\u201901, 2001.","key":"2_CR17"},{"doi-asserted-by":"crossref","unstructured":"P. Hartel. LETOS-a lightweight execution tool for operational semantics. Software-practice and experience, 29:1379\u20131416, September 1999.","key":"2_CR18","DOI":"10.1002\/(SICI)1097-024X(19991225)29:15<1379::AID-SPE286>3.0.CO;2-V"},{"doi-asserted-by":"crossref","unstructured":"P. Hartel and L. Moreau. Formalizing the Safety of Java, the Java Virtual Machine and Java Card. ACM Computing Surveys, 2001. To appear.","key":"2_CR19","DOI":"10.1145\/503112.503115"},{"key":"2_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/3-540-48737-9_9","volume-title":"Formal Syntax and Semantics of Java","author":"P. H. Hartel","year":"1999","unstructured":"P. H. Hartel, M. J. Butler, and M. Levy. The Operational Semantics of a Java Secure Processor. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 313\u2013352. Springer-Verlag, 1999."},{"doi-asserted-by":"crossref","unstructured":"B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java classes. A CM SIGPLAN Notices, 33(10):329\u2013340, October 1998.","key":"2_CR21","DOI":"10.1145\/286942.286973"},{"unstructured":"JavaCard Technology. \n                    http:\/\/java.sun.com\/products\/javacard","key":"2_CR22"},{"unstructured":"J. W. Klop. Term-rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, pages 1\u2013116. Oxford Science Publications, 1992. Volume 2.","key":"2_CR23"},{"unstructured":"X. Leroy, D. Doligez, J. Garrigue, D. R\u00e9my, and J. Vouillon. The Objective Caml system, release 3.00, 2000.","key":"2_CR24"},{"unstructured":"P. M\u00fcller and A. Poetzsch-Heffter. A type system for checking applet isolation in Java Card. In S. Drossopoulou, editor, Formal Techniques for Java Programs, 2001. To appear.","key":"2_CR25"},{"unstructured":"C. Mu\u00f1oz. PBS: Support for the B-method in PVS. Technical Report SRI-CSL-99-01, SRI International, February 1999.","key":"2_CR26"},{"key":"2_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-45315-6_23","volume-title":"Proceedings of FOSSACS\u201901","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."},{"doi-asserted-by":"crossref","unstructured":"T. Nipkow and D. von Oheimb. Java,\/light is type-safe\u2014definitely. In Proceedings of POPL\u201998, pages 161\u2013170. ACM Press, 1998.","key":"2_CR28","DOI":"10.1145\/268946.268960"},{"key":"2_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a generic theorem prover","author":"L. Paulson","year":"1994","unstructured":"L. Paulson. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994."},{"unstructured":"M. Petersson. Compiling Natural Semantics. PhD thesis, Link\u00f6ping University, 1995.","key":"2_CR30"},{"key":"2_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-49059-0_7","volume-title":"Proceedings of 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, Proceedings of TACAS\u201999, volume 1579 of Lecture Notes in Computer Science, pages 89\u2013103. Springer-Verlag, 1999."},{"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. 3","key":"2_CR32"},{"issue":"1","key":"2_CR33","doi-asserted-by":"crossref","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 Transactions on Programming Languages and Systems, 21(1):90\u2013137, January 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"unstructured":"D. Terrasse. Vers un environnement d\u2019aide au developpement de preuves en Semantique Naturelle. PhD thesis, Ecole Nationale des Ponts et Chaussees, 1995.","key":"2_CR34"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:39:17Z","timestamp":1558273157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45418-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426103","9783540454182"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-45418-7_2","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"}}]}}