{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T09:55:03Z","timestamp":1725530103750},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005923"},{"type":"electronic","value":"9783642005930"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00593-0_21","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T10:26:08Z","timestamp":1238149568000},"page":"309-324","source":"Crossref","is-referenced-by-count":1,"title":["Certification of Smart-Card Applications in Common Criteria"],"prefix":"10.1007","author":[{"given":"Iman","family":"Narasamdya","sequence":"first","affiliation":[]},{"given":"Micha\u00ebl","family":"P\u00e9rin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Common Criteria for Information Technology Security Evaluation, Version 3.1, CCMB-2007-09-003 (2007)"},{"issue":"1-3","key":"21_CR2","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.scico.2004.05.011","volume":"55","author":"C.-B. Breunesse","year":"2005","unstructured":"Breunesse, C.-B., Cata\u00f1o, N., Huisman, M., Jacobs, B.: Formal methods for smart cards: an experience report. Sci. Comput. Program.\u00a055(1-3), 53\u201380 (2005)","journal-title":"Sci. Comput. Program."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Chetali, B., Nguyen, Q.-H.: Industrial use of formal methods for a high-level security evaluation. In: Formal Methods, pp. 198\u2013213 (2008)","DOI":"10.1007\/978-3-540-68237-0_15"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Dadeau, F., Potet, M.-L., Tissot, R.: A B formal framework for security developments in the domain of smart card applications. In: Security Conference, pp. 141\u2013155 (2008)","DOI":"10.1007\/978-0-387-09699-5_10"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Proceedings of Symposium in Applied Mathematics, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"21_CR7","first-page":"346","volume-title":"CCS 2006: Proceedings of the 13th ACM conference on Computer and communications security","author":"C.L. Heitmeyer","year":"2006","unstructured":"Heitmeyer, C.L., Archer, M., Leonard, E.I., McLean, J.: Formal specification and verification of data separation in a separation kernel for an embedded system. In: CCS 2006: Proceedings of the 13th ACM conference on Computer and communications security, pp. 346\u2013355. ACM, New York (2006)"},{"issue":"10","key":"21_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. CACM\u00a012(10), 576\u2013580 (1969)","journal-title":"CACM"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-24721-0_8","volume-title":"Fundamental Approaches to Software Engineering","author":"E.-M.G.M. Hubbers","year":"2004","unstructured":"Hubbers, E.-M.G.M., Poll, E.: Reasoning about card tears and transactions in Java Card. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol.\u00a02984, pp. 114\u2013128. Springer, Heidelberg (2004)"},{"key":"21_CR10","unstructured":"Leavens, G., Cheon, Y.: Design by contract with JML (2003)"},{"issue":"1","key":"21_CR11","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111320.1111042","volume":"41","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. SIGPLAN Not.\u00a041(1), 42\u201354 (2006)","journal-title":"SIGPLAN Not."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Narasamdya, I., P\u00e9rin, M.: Certification of smart-card applications in common criteria. Technical Report TR-2008-14, Verimag (September 2008)","DOI":"10.1145\/1529282.1529409"},{"key":"21_CR13","unstructured":"Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy (July 1999)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11813040_2","volume-title":"FM 2006: Formal Methods","author":"G. Schellhorn","year":"2006","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The mondex challenge: Machine checked proofs for an electronic purse. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 16\u201331. Springer, Heidelberg (2006)"},{"key":"21_CR15","unstructured":"Sun Micro systems, Inc, Palo Alto, California. Java Card 3.0 Platform Specification (2008), http:\/\/java.sun.com\/javacard\/3.0\/"},{"key":"21_CR16","unstructured":"Voronkov, A., Narasamdya, I.: Proving inter-program properties. Technical Report TR-2008-13, Verimag (2008)"},{"issue":"3","key":"21_CR17","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1023\/A:1011217102270","volume":"18","author":"M. Wilding","year":"2001","unstructured":"Wilding, M., Greve, D.A., Hardin, D.: Efficient simulation of formal processor models. Formal Methods in System Design\u00a018(3), 233\u2013248 (2001)","journal-title":"Formal Methods in System Design"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-68237-0_5","volume-title":"FM 2008: Formal Methods","author":"A. Zaks","year":"2008","unstructured":"Zaks, A., Pnueli, A.: CoVaC: Compiler validation by program analysis of the cross-product. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 35\u201351. Springer, Heidelberg (2008)"},{"issue":"3","key":"21_CR19","first-page":"223","volume":"9","author":"L.D. Zuck","year":"2003","unstructured":"Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: A methodology for the translation validation of optimizing compilers. J. UCS\u00a09(3), 223\u2013247 (2003)","journal-title":"J. UCS"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00593-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T17:06:36Z","timestamp":1684947996000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00593-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005923","9783642005930"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00593-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}