{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:05:39Z","timestamp":1725559539221},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540278825"},{"type":"electronic","value":"9783540317142"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11526841_21","type":"book-chapter","created":{"date-parts":[[2010,7,18]],"date-time":"2010-07-18T16:51:58Z","timestamp":1279471918000},"page":"302-317","source":"Crossref","is-referenced-by-count":11,"title":["Formal Verification of Security Properties of Smart Card Embedded Source Code"],"prefix":"10.1007","author":[{"given":"June","family":"Andronick","sequence":"first","affiliation":[]},{"given":"Boutheina","family":"Chetali","sequence":"additional","affiliation":[]},{"given":"Christine","family":"Paulin-Mohring","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling (2004) (to appear in print); Online First issue, http:\/\/www.key-project.org\/","DOI":"10.1007\/s10270-004-0058-x"},{"key":"21_CR2","unstructured":"Andronick, J., Chetali, B., Ly, O.: Formal Verification of the Integrity Property in Java Card Technology. In: International Conference on Research in Smart Cards (Esmart 2003) (September 2003)"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/10930755_22","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Andronick","year":"2003","unstructured":"Andronick, J., Chetali, B., Ly, O.: Using Coq to Verify Java Cardformula_image Applet Isolation Properties. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 335\u2013351. Springer, Heidelberg (2003)"},{"key":"21_CR4","unstructured":"The Bali project, http:\/\/isabelle.in.tum.de\/bali\/"},{"key":"21_CR5","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Workshop on Runtime Verification 2001","author":"D. Bartetzko","year":"2001","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass - Java with Assertions. In: Havelund, K., Rosu, G. (eds.) Workshop on Runtime Verification 2001, July 2001. Electronic Notes in Theoretical Computer Science, vol.\u00a055, Elsevier Science, Amsterdam (2001), http:\/\/csd.informatik.uni-oldenburg.de\/~jass\/"},{"key":"21_CR6","unstructured":"Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Pavlova, M.: Enforcing High-Level Security Properties For Applets. In: Sixth Smart Card Research and Advanced Application IFIP Conference (CARDIS 2004) (August 2004)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Serpette, B.P., de Sousa, S.M.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 302\u2013319. Springer, Heidelberg (2001)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-45236-2_7","volume-title":"FME 2003: Formal Methods","author":"D. Bert","year":"2003","unstructured":"Bert, D., Boulm\u00e9, S., Potet, M.-L., Requet, A., Voisin, L.: Adaptable Translator of B Specifications to Embedded C Programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 94\u2013113. Springer, Heidelberg (2003)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"Bornat, R.: Proving Pointer Programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 102\u2013126. Springer, Heidelberg (2000)"},{"key":"21_CR10","first-page":"51","volume-title":"Proceedings of the 2002 International Conference on Dependable Systems and Networks (DSN 2002)","author":"L. Burdy","year":"2002","unstructured":"Burdy, L., Casset, L., Requet, A.: Formal Development of an Embedded Verifier for Java Card Byte Code. In: Proceedings of the 2002 International Conference on Dependable Systems and Networks (DSN 2002), pp. 51\u201358. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Lanet, J.-L., Requet, A.: Java Applet Correctness: A Developer-Oriented Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"21_CR12","unstructured":"Burdy, L., Requet, A.: Jack: Java Applet Correctness Kit (November 2002)"},{"key":"21_CR13","first-page":"23","volume":"7","author":"R. Burstall","year":"1972","unstructured":"Burstall, R.: Some Techniques for Proving Correctness of Programs which Alter Data Structures. Machine Intelligence\u00a07, 23\u201350 (1972)","journal-title":"Machine Intelligence"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-45614-7_17","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"L. Casset","year":"2002","unstructured":"Casset, L.: Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 290\u2013309. Springer, Heidelberg (2002)"},{"key":"21_CR15","unstructured":"The Caveat Project, http:\/\/www-drt.cea.fr\/Pages\/List\/lse\/LSL\/Caveat\/index.html\/"},{"key":"21_CR16","unstructured":"Chetali, B., Loiseaux, C., Gimenez, E., Ly, O.: An Interpretation of the Common Criteria EAL7 level: Formal Modeling of the Java Card Virtual Machine. In: 3rd International Common Criteria Conference (ICCC 2002) (May 2002)"},{"key":"21_CR17","unstructured":"ESC\/Java, http:\/\/research.compaq.com\/SRC\/esc\/"},{"key":"21_CR18","unstructured":"ESC\/Java2, http:\/\/www.sos.cs.ru.nl\/research\/escjava"},{"key":"21_CR19","unstructured":"Filli\u00e2tre, J.-C.: The Why Verification Tool, http:\/\/why.lri.fr\/"},{"issue":"4","key":"21_CR20","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1017\/S095679680200446X","volume":"13","author":"J.-C. Filli\u00e2tre","year":"2003","unstructured":"Filli\u00e2tre, J.-C.: Verification of Non-Functional Programs using Interpretations in Type Theory. Journal of Functional Programming\u00a013(4), 709\u2013745 (2003)","journal-title":"Journal of Functional Programming"},{"key":"21_CR21","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Caduceus tool for the Verification of C Programs, http:\/\/why.lri.fr\/caduceus\/"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-39893-6_18","volume-title":"Formal Methods and Software Engineering","author":"A. Hammad","year":"2003","unstructured":"Hammad, A., Requet, A., Tatibou\u00ebt, B., Voisinet, J.-C.: Java Card Code Generation from B Specifications. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 306\u2013318. Springer, Heidelberg (2003)"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-45719-4_23","volume-title":"Algebraic Methodology and Software Technology","author":"M. Huisman","year":"2002","unstructured":"Huisman, M., Trentelman, K.: Extending JML Specifications with Temporal Logic. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 334\u2013348. Springer, Heidelberg (2002)"},{"key":"21_CR25","first-page":"105","volume-title":"OOPSLA 2000 Companion","author":"G.T. Leavens","year":"2000","unstructured":"Leavens, G.T., Rustan, K., Leino, M., Poll, E., Ruby, C., Jacobs, B.: JML: Notations and Tools Supporting Detailed Design in Java. In: OOPSLA 2000 Companion, October 2000, pp. 105\u2013106. ACM, New York (2000)"},{"key":"21_CR26","unstructured":"Loop, http:\/\/www.sos.cs.ru.nl\/research\/loop"},{"key":"21_CR27","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa Tool for Java Program Verification (2002), http:\/\/krakatoa.lri.fr\/"},{"key":"21_CR28","unstructured":"The PVS system, http:\/\/pvs.csl.sri.com\/"},{"key":"21_CR29","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1109\/ICFEM.2000.873801","volume-title":"Third International Conference on Formal Engineering Methods (ICFEM 2000)","author":"A. Requet","year":"2000","unstructured":"Requet, A., Bossu, G.: Embedding Formally Proved Code in a Smart Card: Converting B to C. In: Third International Conference on Formal Engineering Methods (ICFEM 2000), pp. 15\u201324. IEEE Press, Los Alamitos (2000)"},{"key":"21_CR30","unstructured":"The Simplify decision procedure (part of ESC\/Java), http:\/\/research.compaq.com\/SRC\/esc\/simplify\/Simplify.1.html"},{"key":"21_CR31","unstructured":"Static Source Code Analysis Tools for C, http:\/\/www.spinroot.com\/static\/"},{"key":"21_CR32","unstructured":"The Coq Development Team LogiCal Project. The Coq Proof Assistant Reference Manual, http:\/\/pauillac.inria.fr\/coq\/doc\/main.html"},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D. Oheimb von","year":"1999","unstructured":"von Oheimb, D., Nipkow, T.: Machine-checking the Java Specification: Proving Type-Safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523, pp. 119\u2013156. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","FM 2005: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11526841_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:06:53Z","timestamp":1605643613000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11526841_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278825","9783540317142"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11526841_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}