{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T04:06:25Z","timestamp":1746245185366,"version":"3.40.4"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319064093"},{"type":"electronic","value":"9783319064109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_31","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"449-464","source":"Crossref","is-referenced-by-count":6,"title":["Verification of a Transactional Memory Manager under Hardware Failures and Restarts"],"prefix":"10.1007","author":[{"given":"Ognjen","family":"Mari\u0107","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1.2","key":"31_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1147\/JRD.2011.2178736","volume":"56","author":"T.W. Arnold","year":"2012","unstructured":"Arnold, T.W., Buscaglia, C., Chan, F., Condorelli, V., Dayka, J., Santiago-Fernandez, W., Hadzic, N., Hocker, M.D., Jordan, M., Morris, T., Werner, K.: IBM 4765 cryptographic coprocessor. IBM Journal of Research and Development\u00a056(1.2), 10:1\u201310:13 (2012)","journal-title":"IBM Journal of Research and Development"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Sabatier, D., Lartigue, P.: The use of the B formal method for the design and the validation of the transaction mechanism for smart card applications. Formal Methods in System Design, 245\u2013272 (2000)","DOI":"10.1007\/3-540-48119-2_21"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/3-540-45251-6_28","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"P. Hartel","year":"2001","unstructured":"Hartel, P., Butler, M., de Jong, E., Longley, M.: Transacted memory for smart cards. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 478\u2013499. Springer, Heidelberg (2001)"},{"key":"31_CR4","unstructured":"Poll, E., Hartel, P., de Jong, E.: A Java reference model of transacted memory for smart cards. In: Proceedings of the 5th conference on Smart Card Research and Advanced Application Conference (CARDIS 2002), pp. 1\u201314 (2002)"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"2","key":"31_CR7","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci.\u00a082(2), 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Basin, D.: Refining key establishment. In: Proceedings of Computer Security Foundations Symposium (CSF), pp. 230\u2013246. IEEE (2012)","DOI":"10.1109\/CSF.2012.21"},{"issue":"1","key":"31_CR9","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation\u00a093(1), 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Andronick, J.: Formally proved anti-tearing properties of embedded C code. In: 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), pp. 129\u2013136 (November 2006)","DOI":"10.1109\/ISoLA.2006.14"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-540-74591-4_23","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Sprenger","year":"2007","unstructured":"Sprenger, C., Basin, D.: A monad-based modeling and verification toolbox with application to security protocols. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 302\u2013318. Springer, Heidelberg (2007)"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proc. Principles of Programming Languages (POPL), pp. 14\u201325. ACM (2004)","DOI":"10.1145\/982962.964003"},{"issue":"2","key":"31_CR13","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/s00165-006-0022-3","volume":"19","author":"R. Joshi","year":"2007","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Formal Aspects of Computing\u00a019(2), 269\u2013272 (2007)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:33:54Z","timestamp":1746189234000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}