{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:37Z","timestamp":1761597037602},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540436317"},{"type":"electronic","value":"9783540478133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-47813-2_3","type":"book-chapter","created":{"date-parts":[[2007,5,30]],"date-time":"2007-05-30T22:35:31Z","timestamp":1180564531000},"page":"32-45","source":"Crossref","is-referenced-by-count":17,"title":["A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Guillaume","family":"Dufay","sequence":"additional","affiliation":[]},{"given":"Line","family":"Jakubiec","sequence":"additional","affiliation":[]},{"given":"Sim\u00e3o Melo","family":"de Sousa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,10]]},"reference":[{"key":"3_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":"3_CR2","doi-asserted-by":"crossref","unstructured":"G. Barthe and P. Courtieu. Efficient Reasoning about Executable Specifications in Coq. Manuscript, 2002.","DOI":"10.1007\/3-540-45685-6_4"},{"key":"3_CR3","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":"3_CR4","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":"3_CR5","series-title":"Lect Notes Comput Sci","volume-title":"2002 and model checking for analysing security properties of java bytecode","author":"C. Bernardeschi","year":"2002","unstructured":"C. Bernardeschi and N. De Francesco. Combining abstract interpretation and model checking for analysing security properties of java bytecode. In A. Cortesi, editor, Proceedings of VMCAI\u201902, volume 2xxx of Lecture Notes in Computer Science, 2002."},{"key":"3_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/3-540-44585-4_3","volume-title":"Formalizing in Coq a type system for object initialization in the Java bytecode language","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 2102 of Lecture Notes in Computer Science, pages 14\u201324. Springer-Verlag, 2001."},{"key":"3_CR7","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.","DOI":"10.1016\/S1571-0661(04)00092-1"},{"key":"3_CR8","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, 1999, Fernuniversit\u00e4t Hagen, Fernuniversit\u00e4t Hagen, 1999."},{"key":"3_CR9","unstructured":"R. M. Cohen. Defensive Java Virtual Machine Specification Version 0.5. Manuscript, 1997."},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/3-540-44577-3_10","volume-title":"Informatics \u2014 10 Years Back, 10 Years Ahead","author":"P. Cousot","year":"2001","unstructured":"P. Cousot. Abstract Interpretation Based Formal Methods and Future Challenges. In R. Wilhelm, editor, Informatics \u2014 10 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 138\u2013156. Springer-Verlag, 2001."},{"issue":"6","key":"3_CR11","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 system for 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":"3_CR12","unstructured":"A. Galland, D. Deville, G. Grimaud, and B. Folliot. Contr\u00f4le des ressources dans les cartes \u00e0 microprocesseur. In Proceedings of LTRE\u201902, 2002."},{"key":"3_CR13","unstructured":"P. Girard. Which securityp olicy for multiapplication smart cards? In Proceedings of Usenix workshop on Smart Card Technology (Smartcard\u201999), 1999."},{"key":"3_CR14","doi-asserted-by":"crossref","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:517\u2013558, December 2001.","journal-title":"ACM Computing Surveys"},{"key":"3_CR15","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":"3_CR16","unstructured":"Gemplus Research Labs. Java Card Common Criteria Certification Using Coq. Technical Report, 2001."},{"key":"3_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/10721064_7","volume-title":"Formal Proof of Smart Card Applets Correctness","author":"J.-L. Lanet","year":"2000","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":"3_CR18","unstructured":"M. Montgomery and K. Krishna. Secure Object Sharing in Java Card. In Proceedings of Usenix workshop on Smart Card Technology, (Smartcard\u201999), 1999."},{"key":"3_CR19","unstructured":"J. Strother Moore, R. Krug, H. Liu, and G. Porter. Formal Models of Java at the JVM Level A Surveyf rom the ACL2 Perspective. In S. Drossopoulou, editor, Proceedings of Formal Techniques for Java Programs, 2001."},{"key":"3_CR20","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":"3_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-49059-0_7","volume-title":"Proving the soundness of a Java bytecode verifier specification in Isabelle\/HOL","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."},{"key":"3_CR22","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 J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 271\u2013312. Springer-Verlag, 1999."},{"key":"3_CR23","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":"3_CR24","unstructured":"D.A. Schmidt. Binaryre lations for abstraction and refinement. Technical Report 2000-3, Department of Computing and Information Sciences, Kansas State University, 2000."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"R. St\u00e4rk, J. Schmid, and E. B\u00f6rger. Java and the Java Virtual Machine \u2014 Definition, Verification, Validation. Springer-Verlag, 2001.","DOI":"10.1007\/978-3-642-59495-3"},{"key":"3_CR26","unstructured":"The Coq Development Team. The Coq Proof Assistant User\u2019s Guide. Version 7.2, January 2002."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47813-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T09:36:28Z","timestamp":1556444188000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47813-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540436317","9783540478133"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-47813-2_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}