{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:23:48Z","timestamp":1763054628468,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T00:00:00Z","timestamp":1760313600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["1844964"],"award-info":[{"award-number":["1844964"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3764860.3768337","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T13:54:43Z","timestamp":1759326883000},"page":"25-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Modal Verification Patterns for Systems Software"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5796-2150","authenticated-orcid":false,"given":"Ismail","family":"Kuru","sequence":"first","affiliation":[{"name":"Drexel University, Philadelphia, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9012-4490","authenticated-orcid":false,"given":"Colin S.","family":"Gordon","sequence":"additional","affiliation":[{"name":"Drexel University, Philadelphia, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,13]]},"reference":[{"volume-title":"Actors: a model of concurrent computation in distributed systems","author":"Agha Gul","key":"e_1_3_2_1_1_1","unstructured":"Gul Agha. 1986. Actors: a model of concurrent computation in distributed systems. MIT press."},{"volume-title":"Go Where the Bugs Are: Essays Dedicated to Wolfgang Reif on the Occasion of His 65th Birthday","author":"Ahrendt Wolfgang","key":"e_1_3_2_1_2_1","unstructured":"Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H \u00e4hnle, and Mattias Ulbrich. 2025. The Many Uses of Dynamic Logic. In Go Where the Bugs Are: Essays Dedicated to Wolfgang Reif on the Occasion of His 65th Birthday. Springer, 56--82."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695090"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01049415"},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. of the 2nd Usenix Conference on File and Storage Technologies (USENIX FAST).","author":"Bonwick Jeff","year":"2003","unstructured":"Jeff Bonwick, Matt Ahrens, Val Henson, Mark Maybee, and Mark Shellenbaum. 2003. The Zettabyte File System. In Proc. of the 2nd Usenix Conference on File and Storage Technologies (USENIX FAST)."},{"volume-title":"Hybrid logic and its proof-theory","author":"Bra\u00fcner Torben","key":"e_1_3_2_1_6_1","unstructured":"Torben Bra\u00fcner. 2010. Hybrid logic and its proof-theory. Vol. 37. Springer Science & Business Media."},{"key":"e_1_3_2_1_7_1","unstructured":"Tej Chajed. 2022. Verifying a concurrent crash-safe file system with sequential reasoning. Ph.D. Dissertation. Machetutes Institute of Technology Cambridge MA. Available at https:\/\/dspace.mit.edu\/handle\/1721.1\/144578."},{"key":"e_1_3_2_1_8_1","unstructured":"Tej Chajed Joseph Tassarotti and Contributors. 2023. Post-crash modality in Perennial's Coq Mechanization. https:\/\/github.com\/mit-pdos\/perennial\/blob\/master\/src\/goose_lang\/crash_modality.v"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the USENIX","author":"Chutani Sailesh","year":"1992","unstructured":"Sailesh Chutani, Owen T Anderson, Michael L Kazar, Bruce W Leverett, W Anthony Mason, and Robert N Sidebotham. 1992. The Episode file system. In Proceedings of the USENIX Winter 1992 Technical Conference. San Fransisco, CA, USA, 43--60."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/356571.356573"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260931"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01054038"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00215625"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3358499.3361221"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/41457.37518"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544585.3544593"},{"volume-title":"Reasoning about uncertainty","author":"Halpern Joseph Y","key":"e_1_3_2_1_24_1","unstructured":"Joseph Y Halpern. 2017. Reasoning about uncertainty. MIT press."},{"key":"e_1_3_2_1_25_1","volume-title":"Modelling knowledge and action in distributed systems. Distributed computing 3","author":"Halpern Joseph Y","year":"1989","unstructured":"Joseph Y Halpern and Ronald Fagin. 1989. Modelling knowledge and action in distributed systems. Distributed computing 3 (1989), 159--177."},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the 9th international joint conference on Artificial intelligence-Volume 1. Morgan Kaufmann Publishers Inc., 480--490","author":"Halpern Joseph Y","year":"1985","unstructured":"Joseph Y Halpern and Yoram Moses. 1985. A guide to the modal logics of knowledge and belief. In Proceedings of the 9th international joint conference on Artificial intelligence-Volume 1. Morgan Kaufmann Publishers Inc., 480--490."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/79147.79161"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512942"},{"volume-title":"Knowledge and belief","author":"Hintikka Jaakko","key":"e_1_3_2_1_29_1","unstructured":"Jaakko Hintikka. 1962. Knowledge and belief. Cornell University Press."},{"key":"e_1_3_2_1_30_1","volume-title":"USENIX Winter","volume":"94","author":"Hitz Dave","year":"1994","unstructured":"Dave Hitz, James Lau, and Michael A Malcolm. 1994. File System Design for an NFS File Server Appliance.. In USENIX Winter, Vol. 94."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/35037.42182"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019915908844"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Robert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Principles of Programming Languages (POPL). http:\/\/cs.au.dk\/~birke\/papers\/ipm-conf.pdf","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763134"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_1_39_1","volume-title":"Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning","author":"Leino K Rustan M","year":"2010","unstructured":"K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. Springer, 348--370."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319623"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Hiroshi Nakano. 2000. A Modality for Recursion. In Logic in Computer Science (LICS). 255--266. http:\/\/www602.math.ryukoku.ac.jp\/~nakano\/papers\/modality-lics00.ps.gz","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"volume-title":"Theorem Proving in Higher Order Logics","author":"Owens Scott","key":"e_1_3_2_1_43_1","unstructured":"Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A better x86 memory model: x86-TSO. In Theorem Proving in Higher Order Logics. Springer, 391--407."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_45_1","volume-title":"Foundations of Computer Science, 1976., 17th Annual Symposium on. IEEE, 109--121","author":"Pratt Vaughan R","year":"1976","unstructured":"Vaughan R Pratt. 1976. Semantical consideration on Floyd-Hoare logic. In Foundations of Computer Science, 1976., 17th Annual Symposium on. IEEE, 109--121."},{"key":"e_1_3_2_1_46_1","volume-title":"Modalities in substructural logics. Logique et Analyse 36, 141\/142","author":"Restall Greg","year":"1993","unstructured":"Greg Restall. 1993. Modalities in substructural logics. Logique et Analyse 36, 141\/142 (1993), 25--38."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.4324\/9780203252642"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2501620.2501623"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/146941.146943"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_30"},{"key":"e_1_3_2_1_52_1","volume-title":"Typestate: A programming language concept for enhancing software reliability","author":"Strom Robert E","year":"1986","unstructured":"Robert E Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE transactions on software engineering 1 (1986), 157--171."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3703595.3705876"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689755"}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Seoul Republic of Korea","acronym":"SOSP '25"},"container-title":["Proceedings of the 13th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3764860.3768337","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768337","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:20:39Z","timestamp":1763054439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764860.3768337"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,13]]},"references-count":54,"alternative-id":["10.1145\/3764860.3768337","10.1145\/3764860"],"URL":"https:\/\/doi.org\/10.1145\/3764860.3768337","relation":{},"subject":[],"published":{"date-parts":[[2025,10,13]]},"assertion":[{"value":"2025-10-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}