{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:13:13Z","timestamp":1748405593928,"version":"3.41.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031921957","type":"print"},{"value":"9783031921964","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-92196-4_16","type":"book-chapter","created":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:23:20Z","timestamp":1748348600000},"page":"325-355","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mirror is Not Strong: Discovery of\u00a0a\u00a0Persistent Memory Bug using Refinement in\u00a0KIV"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6712-7178","authenticated-orcid":false,"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4596-2305","authenticated-orcid":false,"given":"Stefan","family":"Bodenm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,28]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Bila, E.,\u00a0Derrick, J.,\u00a0Doherty, S.,\u00a0Dongol, B.,\u00a0Schellhorn, G.,\u00a0Wehrheim, H.: Modularising verification of durable opacity. Log. Methods Comput. Sci. 18(3) (2022). https:\/\/doi.org\/10.46298\/lmcs-18(3:7)2022","DOI":"10.46298\/lmcs-18(3:7)2022"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Bila, E.,\u00a0Doherty, S.,\u00a0Dongol, B.,\u00a0Derrick, J.,\u00a0Schellhorn, G.,\u00a0Wehrheim, H.: Defining and verifying durable opacity: correctness for persistent software transactional memory. In:\u00a0Gotsman, A.,\u00a0Sokolova, A. (eds.) FORTE, LNCS, vol. 12136, pp. 39\u201358. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_3","DOI":"10.1007\/978-3-030-50086-3_3"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Bodenm\u00fcller, S.,\u00a0Derrick, J.,\u00a0Dongol, B.,\u00a0Schellhorn, G.,\u00a0Wehrheim, H.: A fully verified persistency library. In: VMCAI (2), vol. 14500 of Lecture Notes in Computer Science, pp. 26\u201347. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-50521-8_2","DOI":"10.1007\/978-3-031-50521-8_2"},{"key":"16_CR4","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.scico.2024.103227","volume":"241","author":"S Bodenm\u00fcller","year":"2024","unstructured":"Bodenm\u00fcller, S., Schellhorn, G., Reif, W.: Verification of forward simulations with thread-local, step-local proof obligations. Sci. Comput. Program. 241, 103\u2013227 (2024). https:\/\/doi.org\/10.1016\/j.scico.2024.103227","journal-title":"Sci. Comput. Program."},{"issue":"10","key":"16_CR5","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1145\/2714064.2660224","volume":"49","author":"DR Chakrabarti","year":"2014","unstructured":"Chakrabarti, D.R., Boehm, H.-J., Bhandari, K.: Atlas: leveraging locks for non-volatile memory consistency. ACM SIGPLAN Not. 49(10), 433\u2013452 (2014)","journal-title":"ACM SIGPLAN Not."},{"key":"16_CR6","unstructured":"compare_exchange as defined in the C++ standard library (2024). https:\/\/en.cppreference.com\/w\/cpp\/atomic\/atomic\/compare_exchange"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Wehrheim, H.: Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput. 547\u2013573 (2021). https:\/\/doi.org\/10.1007\/s00165-021-00541-8","DOI":"10.1007\/s00165-021-00541-8"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Proving linearizability via non-atomic refinement. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 195\u2013214. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73210-5_11","DOI":"10.1007\/978-3-540-73210-5_11"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanizing a correctness proof for a lock-free concurrent stack. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 78\u201395. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_6","DOI":"10.1007\/978-3-540-68863-1_6"},{"issue":"1","key":"16_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1889997.1890001","volume":"33","author":"J Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1), 1\u201343 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Derrick, J.,\u00a0Schellhorn, G.,\u00a0Wehrheim, H.: Verifying linearisability with potential linearisation points. In: Butler, M.J.,\u00a0Schulte, W. (eds.) FM, volume 6664 of LNCS, pp. 323\u2013337. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_25","DOI":"10.1007\/978-3-642-21437-0_25"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Doherty, S.,\u00a0Groves, L.,\u00a0Luchangco, V.,\u00a0Moir, M.: Formal verification of a practical lock-free queue algorithm. In: FORTE, volume 3235 of LNCS, pp. 97\u2013114. Springer (2004)","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"D\u2019Osualdo, E.,\u00a0Raad, A.,\u00a0Vafeiadis, V.: The path to durable linearizability. Proc. ACM Program. Lang. 7(POPL), 748\u2013774 (2023). https:\/\/doi.org\/10.1145\/3571219","DOI":"10.1145\/3571219"},{"key":"16_CR14","unstructured":"Egorov, S., Chockler, G.V.,\u00a0Dongol, B.,\u00a0O\u2019Keeffe, D.,\u00a0Keshavarzi, S.: Mangosteen: fast transparent durability for linearizable applications using NVM. In:\u00a0Bagchi, S.,\u00a0Zhang, Y. (eds.) Proceedings of the 2024 USENIX Annual Technical Conference, USENIX ATC 2024, Santa Clara, CA, USA, July 10\u201312, 2024, pp. 799\u2013815. USENIX Association (2024). https:\/\/www.usenix.org\/conference\/atc24\/presentation\/egorov"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Friedman, M.,\u00a0Ben-David, N.,\u00a0Wei, Y., Blelloch, G.E.,\u00a0Petrank, E.: NVTraverse: in NVRAM data structures, the destination is more important than the journey. In: Donaldson, A.F.,\u00a0Torlak, E. (eds.) PLDI, pp. 377\u2013392. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3386031","DOI":"10.1145\/3385412.3386031"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Friedman, M.,\u00a0Petrank, E.,\u00a0Ramalhete, P.: Mirror: making lock-free data structures persistent. In: Freund, S.N.,\u00a0Yahav, E. (eds.) PLDI, pp. 1218\u20131232. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454105","DOI":"10.1145\/3453483.3454105"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.,\u00a0Heisel, M.,\u00a0Reif, W.,\u00a0Stephan, W.: An interactive verification system based on dynamic logic. In: Proceedings of the 8th International Conference on Automated Deduction, pp. 306-315. Springer (1986)","DOI":"10.1007\/3-540-16780-3_99"},{"issue":"3","key":"16_CR18","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS 12(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Izraelevitz, J.,\u00a0Mendes, H., Scott, M.L.: Linearizability of persistent memory objects under a full-system-crash failure model. In:\u00a0Gavoille, C.,\u00a0Ilcinkas, D. (eds.) DISC, volume 9888 of LNCS, pp. 313\u2013327. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-53426-7_23","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Khyzha, A.,\u00a0Lahav, O.: Taming $$\\times $$86-TSO persistency. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434328","DOI":"10.1145\/3434328"},{"issue":"2","key":"16_CR21","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations. Inf. Comput. 121(2), 214\u2013233 (1995)","journal-title":"Inf. Comput."},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"WDAG 1996. LNCS, vol. 1151. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61769-8_9","DOI":"10.1007\/3-540-61769-8_9"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137\u2013151. ACM, New York, NY, USA (1987)","DOI":"10.1145\/41840.41852"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Memaripour, A.S.,\u00a0Izraelevitz, J.,\u00a0Swanson, S.: Pronto: easy and fast persistence for volatile data structures. In: Larus, J.R.,\u00a0Ceze, L.,\u00a0Strauss, K. (eds.) ASPLOS \u201920: Architectural Support for Programming Languages and Operating Systems, Lausanne, Switzerland, March 16\u201320, 2020, pp. 789\u2013806. ACM (2020). https:\/\/doi.org\/10.1145\/3373376.3378456","DOI":"10.1145\/3373376.3378456"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC, pp. 267\u2013275. ACM (1996)","DOI":"10.1145\/248052.248106"},{"key":"16_CR26","doi-asserted-by":"publisher","unstructured":"Raad, A.,\u00a0Lahav, O.,\u00a0Wickerson, J.,\u00a0Balcer, P.,\u00a0Dongol, B.: Intel PMDK transactions: specification, validation and concurrency. In:\u00a0Weirich, S. (ed.) ESOP, volume 14577 of LNCS, pp. 150\u2013179. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57267-8_6","DOI":"10.1007\/978-3-031-57267-8_6"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Raad, A.,\u00a0Wickerson, J.,\u00a0Neiger, G.,\u00a0Vafeiadis, V.: Persistency semantics of the intel-x86 architecture. Proc. ACM Program. Lang. 4(POPL), 11:1\u201311:31 (2020). https:\/\/doi.org\/10.1145\/3371079","DOI":"10.1145\/3371079"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Scargall, S.: Programming Persistent Memory: A Comprehensive Guide for Developers. Springer Nature (2020)","DOI":"10.1007\/978-1-4842-4932-1"},{"key":"16_CR29","unstructured":"Schellhorn, G.,\u00a0Bodenm\u00fcller, S.,\u00a0Dongol, B.,\u00a0Wehrheim, H.: Verification of correctness of the MIRROR persistence library (2024). http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/MIRROR.html"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Schellhorn, G.,\u00a0Derrick, J.,\u00a0Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Log. 15(4), 31:1\u201331:37 (2014). https:\/\/doi.org\/10.1145\/2629496","DOI":"10.1145\/2629496"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Wehrheim, H., Derrick, J.: How to prove algorithms linearisable. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 243\u2013259. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_21","DOI":"10.1007\/978-3-642-31424-7_21"},{"issue":"2","key":"16_CR32","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s004460050028","volume":"10","author":"N Shavit","year":"1997","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. Distrib. Comput. 10(2), 99\u2013116 (1997)","journal-title":"Distrib. Comput."},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Stefanesco, L.,\u00a0Raad, A.,\u00a0Vafeiadis, V.: Specifying and verifying persistent libraries. In: ESOP (2), volume 14577 of LNCS, pp. 185\u2013211. Springer (2024)","DOI":"10.1007\/978-3-031-57267-8_8"},{"key":"16_CR34","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/j.scico.2014.04.001","volume":"96","author":"B Tofan","year":"2014","unstructured":"Tofan, B., Travkin, O., Schellhorn, G., Wehrheim, H.: Two approaches for proving linearizability of multiset. Sci. Comput. Program. 96, 297\u2013314 (2014)","journal-title":"Sci. Comput. Program."},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Wei, Y.,\u00a0Ben-David, N.,\u00a0Friedman, M., Blelloch, G.E.,\u00a0Petrank, E.: FliT: a library for simple and efficient persistent algorithms. In:\u00a0Lee, J.,\u00a0Agrawal, K., Spear, M.F. (eds.) PPoPP, pp. 309\u2013321. ACM (2022). https:\/\/doi.org\/10.1145\/3503221.3508436","DOI":"10.1145\/3503221.3508436"},{"key":"16_CR36","doi-asserted-by":"publisher","unstructured":"Wen, H.,\u00a0Cai, W.,\u00a0Du, M.,\u00a0Jenkins, L.,\u00a0Valpey, B., Scott, M.L.: A fast, general system for buffered persistent data structures. In: Sun, X.-H.,\u00a0Shende, S., Kal\u00e9, L.V.,\u00a0Chen, Y. (eds.) ICPP, pp. 73:1\u201373:11. ACM (2021). https:\/\/doi.org\/10.1145\/3472456.3472458","DOI":"10.1145\/3472456.3472458"},{"key":"16_CR37","unstructured":"Zhang, W.,\u00a0Shenker, S.,\u00a0Zhang, I.: Persistent state machines for recoverable in-memory storage systems with NVRAM. In: 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4\u20136, 2020, pp. 1029\u20131046. USENIX Association (2020). https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/zhang-wen"}],"container-title":["Lecture Notes in Computer Science","Go Where the Bugs Are"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-92196-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:23:23Z","timestamp":1748348603000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-92196-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031921957","9783031921964"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-92196-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"28 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}