{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:08:50Z","timestamp":1781258930454,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":88,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,11,4]],"date-time":"2024-11-04T00:00:00Z","timestamp":1730678400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CCF 231895"],"award-info":[{"award-number":["CCF 231895"]}]},{"name":"AFRL, DARPA","award":["FA8750-24-9-1000"],"award-info":[{"award-number":["FA8750-24-9-1000"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,11,4]]},"DOI":"10.1145\/3694715.3695952","type":"proceedings-article","created":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T19:28:18Z","timestamp":1731698898000},"page":"438-454","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Verus: A Practical Foundation for Systems Verification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9303-452X","authenticated-orcid":false,"given":"Andrea","family":"Lattuada","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, DE"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-1104-7795","authenticated-orcid":false,"given":"Travis","family":"Hance","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, US"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5596-6828","authenticated-orcid":false,"given":"Jay","family":"Bosamiya","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, US"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5349-4347","authenticated-orcid":false,"given":"Matthias","family":"Brun","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, CH"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-6620-9070","authenticated-orcid":false,"given":"Chanhee","family":"Cho","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, US"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3680-496X","authenticated-orcid":false,"given":"Hayley","family":"LeBlanc","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, US"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7162-5442","authenticated-orcid":false,"given":"Pranav","family":"Srinivasan","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, US"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3263-7236","authenticated-orcid":false,"given":"Reto","family":"Achermann","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, BC, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9889-4828","authenticated-orcid":false,"given":"Tej","family":"Chajed","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, WI, US"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-0362","authenticated-orcid":false,"given":"Chris","family":"Hawblitzel","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1781-2473","authenticated-orcid":false,"given":"Jon","family":"Howell","sequence":"additional","affiliation":[{"name":"VMware Research, Bellevue, WA, US"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7269-2769","authenticated-orcid":false,"given":"Jacob R.","family":"Lorch","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, US"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[{"name":"Weizmann Institute of Science, Rehovot, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9113-1684","authenticated-orcid":false,"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, US"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,11,15]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-button verification of file systems via crash refinement. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), November 2016."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_2_4_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Nelson Luke","year":"2017","unstructured":"Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2017."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_2_6_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Nelson Luke","year":"2020","unstructured":"Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), November 2020."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_2_8_1","volume-title":"Proceedings of the Conference on Computer Aided Verification (CAV)","author":"Kenneth","year":"2020","unstructured":"Kenneth L. McMillan and Oded Padon. Ivy: A multi-modal verification tool for distributed algorithms. In Proceedings of the Conference on Computer Aided Verification (CAV), 2020."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_2_12_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), October 2014."},{"key":"e_1_3_2_2_13_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Hawblitzel Chris","year":"2015","unstructured":"Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. IronFleet: Proving practical distributed systems correct. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October 2015."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_2_2_15_1","volume-title":"Proceedings of the ACM Conference on Computer and Communications Security (CCS)","author":"Polubelova Marina","year":"2020","unstructured":"Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, and Santiago Zanella-B\u00e9guelin. HACL\u00d7N: Verified generic SIMD crypto (for all your favorite platforms). In Proceedings of the ACM Conference on Computer and Communications Security (CCS), October 2020."},{"key":"e_1_3_2_2_16_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hance Travis","year":"2020","unstructured":"Travis Hance, Andrea Lattuada, C. Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. Storage systems are distributed systems (so verify them that way!). In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2020."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9161-6"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_3_2_2_20_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. Finding invariants of distributed systems: It's a small (enough) world after all. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), April 2021."},{"key":"e_1_3_2_2_21_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2022."},{"key":"e_1_3_2_2_22_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. DistAI: Data-Driven automated invariant learning for distributed protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2021."},{"key":"e_1_3_2_2_23_1","unstructured":"The Verus Contributors. Verus repository. https:\/\/github.com\/verus-lang\/verus."},{"key":"e_1_3_2_2_24_1","volume-title":"Verus SOSP artifact. https:\/\/verus-lang.github.io\/papersosp24-artifact\/","author":"Lattuada Andrea","year":"2024","unstructured":"Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon, and Bryan Parno. Verus SOSP artifact. https:\/\/verus-lang.github.io\/papersosp24-artifact\/, 2024."},{"key":"e_1_3_2_2_25_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sun Xudong","year":"2024","unstructured":"Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. Anvil: Verifying liveness of cluster management controllers. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2024."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3625275.3625401"},{"key":"e_1_3_2_2_27_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhou Ziqiao","year":"2024","unstructured":"Ziqiao Zhou, Weiteng Chen, Chris Hawblitzel, and Weidong Cui. VeriSMo: A verified security module for confidential VMs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2024."},{"key":"e_1_3_2_2_28_1","volume-title":"Leveraging large language models for automated proof synthesis in Rust. https:\/\/arxiv.org\/abs\/2311.03739","author":"Yao Jianan","year":"2023","unstructured":"Jianan Yao, Ziqiao Zhou, Weiteng Chen, and Weidong Cui. Leveraging large language models for automated proof synthesis in Rust. https:\/\/arxiv.org\/abs\/2311.03739, 2023."},{"key":"e_1_3_2_2_29_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hance Travis","year":"2023","unstructured":"Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. Sharding the state machine: Automated modular reasoning for complex concurrent systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2023."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_2_2_31_1","unstructured":"Coq Development Team. The Coq Proof Assistant https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_2_32_1","volume-title":"Proceedings of the Conference on Automated Deduction (CADE)","author":"de Moura Leonardo","year":"2015","unstructured":"Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover. In Proceedings of the Conference on Automated Deduction (CADE), August 2015."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_2_35_1","volume-title":"Proceedings of the ACM Conference on Principles of Programming Languages (POPL)","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy, C\u0103t\u0103lin Hri\u0163cu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohou\u00e9, and Santiago Zanella-B\u00e9guelin. Dependent types and multi-monadic effects in F\u2605. In Proceedings of the ACM Conference on Principles of Programming Languages (POPL), 2016."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_3_2_2_37_1","volume-title":"USA","author":"Klabnik Steve","year":"2018","unstructured":"Steve Klabnik and Carol Nichols. The Rust Programming Language. No Starch Press, USA, 2018."},{"key":"e_1_3_2_2_38_1","volume-title":"October","author":"Proven Liam","year":"2022","unstructured":"Liam Proven. Linux 6.1: Rust to hit mainline kernel. https:\/\/www.theregister.com\/2022\/10\/05\/rust_kernel_pull_request_pulled\/, October 2022."},{"key":"e_1_3_2_2_39_1","volume-title":"February","author":"Miller Shane","year":"2022","unstructured":"Shane Miller and Carl Lerche. Sustainability with Rust. https:\/\/aws.amazon.com\/blogs\/opensource\/sustainability-with-rust\/, February 2022."},{"key":"e_1_3_2_2_40_1","volume-title":"October","year":"2022","unstructured":"Google. Announcing KataOS and Sparrow. https:\/\/opensource.googleblog.com\/2022\/10\/announcing-kataos-and-sparrow.html, October 2022."},{"key":"e_1_3_2_2_41_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Bae Yechan","year":"2021","unstructured":"Yechan Bae, Youngsuk Kim, Ammar Askar, Jungwon Lim, and Taesoo Kim. RUDRA: Finding memory safety bugs in Rust at the ecosystem scale. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October 2021."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3502491"},{"key":"e_1_3_2_2_43_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October 2017."},{"key":"e_1_3_2_2_44_1","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference","author":"Zhou Yi","year":"2023","unstructured":"Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, and Bryan Parno. Mariposa: Measuring SMT instability in automated program verification. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference, October 2023."},{"key":"e_1_3_2_2_45_1","volume-title":"Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers. Addison-Wesley, 2002."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_2_48_1","first-page":"12","author":"Hoare Tony","year":"1969","unstructured":"Tony Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12, 1969.","journal-title":"Communications of the ACM"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670416"},{"key":"e_1_3_2_2_50_1","volume-title":"Reducing liveness to safety in first-order logic. PACMPL, 2(POPL):26:1--26:33","author":"Padon Oded","year":"2018","unstructured":"Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Reducing liveness to safety in first-order logic. PACMPL, 2(POPL):26:1--26:33, 2018."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_18"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134076"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616603"},{"key":"e_1_3_2_2_54_1","volume-title":"December","author":"Lorch Jacob R.","year":"2023","unstructured":"Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Haojun Ma, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao. Armada code repository. https:\/\/github.com\/microsoft\/Armada\/blob\/ee799110f9aecc3deab31b94521bdbcd27f58363\/Test\/qbss\/bv.dfy#L54, December 2023."},{"key":"e_1_3_2_2_55_1","volume-title":"February","author":"Oostdijk Martijn","year":"2002","unstructured":"Martijn Oostdijk and Herman Geuvers. Proof by computation in the Coq system. Theoretical Computer Science, 272(1--2), February 2002."},{"key":"e_1_3_2_2_56_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP)","author":"Mart\u00ednez Guido","year":"2019","unstructured":"Guido Mart\u00ednez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Cl\u00e9ment Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. Meta-F*: Proof automation with SMT, tactics, and metaprograms. In Proceedings of the European Symposium on Programming (ESOP), April 2019."},{"key":"e_1_3_2_2_57_1","first-page":"28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung, R. Krebbers, Jacques-Henri Jourdan, A. Bizjak, L. Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28, 2018.","journal-title":"Journal of Functional Programming"},{"key":"e_1_3_2_2_58_1","volume-title":"April","author":"O'Hearn Peter W.","year":"2007","unstructured":"Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theoretical Computer Science, 375(1--3), April 2007."},{"key":"e_1_3_2_2_59_1","volume-title":"Proceedings of the USENIX Security Symposium","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. Vale: Verifying high-performance cryptographic assembly code. In Proceedings of the USENIX Security Symposium, August 2017."},{"key":"e_1_3_2_2_60_1","volume-title":"September","author":"Protzenko Jonathan","year":"2017","unstructured":"Jonathan Protzenko, Jean-Karim Zinzindohou\u00e9, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-B\u00e9guelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, C\u00e9dric Fournet, and Nikhil Swamy. Verified low-level programming embedded in F*. PACMPL, 1(ICFP), September 2017."},{"key":"e_1_3_2_2_61_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Markulf Kohlweiss, Jiangyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-B\u00e9guelin, and Jean Karim Zinzindohou\u00e9. Implementing and proving the TLS 1.3 record layer. In Proceedings of the IEEE Symposium on Security and Privacy, May 2017."},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00039"},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00064"},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"},{"key":"e_1_3_2_2_65_1","volume-title":"Proceedings of the International Conference on Formal Engineering Methods","author":"Denis Xavier","year":"2022","unstructured":"Xavier Denis, Jacques-Henri Jourdan, and Claude March\u00e9. Creusot: A foundry for the deductive verication of Rust programs. In Proceedings of the International Conference on Formal Engineering Methods, October 2022."},{"key":"e_1_3_2_2_66_1","volume-title":"IronFleet code. https:\/\/research.microsoft.com\/projects\/ironclad\/","author":"Hawblitzel Chris","year":"2015","unstructured":"Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Haojun Ma, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. IronFleet code. https:\/\/research.microsoft.com\/projects\/ironclad\/, 2015."},{"key":"e_1_3_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527313"},{"key":"e_1_3_2_2_68_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Bhardwaj Ankit","year":"2021","unstructured":"Ankit Bhardwaj, Chinmay Kulkarni, Reto Achermann, Irina Calciu, Sanidhya Kashyap, Ryan Stutsman, Amy Tai, and Gerd Zellweger. NrOS: Effective replication and sharing in an operating system. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2021."},{"key":"e_1_3_2_2_69_1","volume-title":"Bryan Parno. IronSync OSDI 2023 artifact. https:\/\/github.com\/secure-foundations\/ironsync-osdi2023","author":"Hance Travis","year":"2023","unstructured":"Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. IronSync OSDI 2023 artifact. https:\/\/github.com\/secure-foundations\/ironsync-osdi2023, 2023."},{"key":"e_1_3_2_2_71_1","volume-title":"https:\/\/github.com\/daanx\/mimalloc-bench","author":"Leijen Daan","year":"2023","unstructured":"Daan Leijen. Mimalloc-bench. https:\/\/github.com\/daanx\/mimalloc-bench, 2023."},{"key":"e_1_3_2_2_72_1","unstructured":"Intel. Intel Optane persistent memory. https:\/\/www.intel.com\/content\/www\/us\/en\/products\/docs\/memory-storage\/optane-persistent-memory\/overview.html."},{"key":"e_1_3_2_2_73_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles, (SOSP)","author":"Xu Jian","year":"2017","unstructured":"Jian Xu, Lu Zhang, Amirsaman Memaripour, Akshatha Gangadharaiah, Amit Borase, Tamires Brito Da Silva, Steven Swanson, and Andy Rudoff. NOVA-Fortis: A fault-tolerant non-volatile main memory file system. In Proceedings of the ACM Symposium on Operating Systems Principles, (SOSP), 2017."},{"key":"e_1_3_2_2_74_1","unstructured":"Linux Kernel Developers. Direct Access for files. https:\/\/www.kernel.org\/doc\/Documentation\/filesystems\/dax.txt."},{"key":"e_1_3_2_2_75_1","unstructured":"PMDK Developers. libpmemlog. https:\/\/pmem.io\/pmdk\/manpages\/linux\/v1.3\/libpmemlog.3\/."},{"key":"e_1_3_2_2_76_1","unstructured":"PMDK Developers. PMDK. https:\/\/pmem.io\/pmdk\/."},{"key":"e_1_3_2_2_77_1","volume-title":"Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)","author":"Kumar Ramana","year":"2014","unstructured":"Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), January 2014."},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_2_79_1","volume-title":"Formal verification of a realistic compiler. Communications of the ACM (CACM), 52(7):107--115","author":"Leroy Xavier","year":"2009","unstructured":"Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM (CACM), 52(7):107--115, 2009."},{"key":"e_1_3_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_2_81_1","volume-title":"Proceedings of the USENIX Conference on Operating Systems Design and Implementation (OSDI)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the USENIX Conference on Operating Systems Design and Implementation (OSDI), 2016."},{"key":"e_1_3_2_2_82_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Li Xupeng","year":"2023","unstructured":"Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh. Spoq: Scaling machine-checkable systems verification in Coq. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2023."},{"key":"e_1_3_2_2_83_1","volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002."},{"key":"e_1_3_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_85_1","volume-title":"Proceedings of the ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Amani Sidney","year":"2016","unstructured":"Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. Cogent: Verifying high-assurance file system implementations. In Proceedings of the ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2016."},{"key":"e_1_3_2_2_86_1","volume-title":"Linear types can change the world! In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. Linear types can change the world! In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods, 1990."},{"key":"e_1_3_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"}],"event":{"name":"SOSP '24: ACM SIGOPS 30th Symposium on Operating Systems Principles","location":"Austin TX USA","acronym":"SOSP '24","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3694715.3695952","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3694715.3695952","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:47Z","timestamp":1750291547000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3694715.3695952"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,4]]},"references-count":88,"alternative-id":["10.1145\/3694715.3695952","10.1145\/3694715"],"URL":"https:\/\/doi.org\/10.1145\/3694715.3695952","relation":{},"subject":[],"published":{"date-parts":[[2024,11,4]]},"assertion":[{"value":"2024-11-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}