{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:47:59Z","timestamp":1759366079899,"version":"build-2065373602"},"publisher-location":"New York, NY, USA","reference-count":113,"publisher":"ACM","funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-2107147","CNS-2321726","CNS-2326576","CNS-2045861","CNS-2321725","CNS-2238768","CNS-2130590"],"award-info":[{"award-number":["CNS-2107147","CNS-2321726","CNS-2326576","CNS-2045861","CNS-2321725","CNS-2238768","CNS-2130590"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"State University of New York (SUNY) Empire Innovation Award"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3731569.3764822","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:43:24Z","timestamp":1759322604000},"page":"768-785","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["AutoMan: Facilitating Verified Distributed Systems Development Through Automatic Code Generation and Manual Optimizations"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-3138-3901","authenticated-orcid":false,"given":"Zihao","family":"Zhang","sequence":"first","affiliation":[{"name":"Stony Brook University, Stony Brook, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2871-3785","authenticated-orcid":false,"given":"Ti","family":"Zhou","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5434-5018","authenticated-orcid":false,"given":"Christa","family":"Jenkins","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1356-6279","authenticated-orcid":false,"given":"Omar","family":"Chowdhury","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8244-2109","authenticated-orcid":false,"given":"Shuai","family":"Mu","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Abhashkumar Anubhavnidhi","year":"2020","unstructured":"Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. Tiramisu: Fast multilayer network verification. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020."},{"key":"e_1_3_2_1_2_1","volume-title":"Techniques & Tools.","author":"Alfred V Aho","year":"2007","unstructured":"V Aho Alfred, S Lam Monica, and D Ullman Jeffrey. Compilers Principles, Techniques & Tools. 2007."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Alquraan Ahmed","year":"2018","unstructured":"Ahmed Alquraan, Hatem Takruri, Mohammed Alfatafta, and Samer Al-Kiswany. An analysis of network-partitioning failures in cloud systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2018."},{"key":"e_1_3_2_1_4_1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur, Rastislav Bod\u00edk, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), 2013."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1007\/BF01213601","article-title":"Reasoning about Prolog programs: From modes through types to assertions","volume":"6","author":"Apt Krzysztof R.","year":"1994","unstructured":"Krzysztof R. Apt and Elena Marchiori. Reasoning about Prolog programs: From modes through types to assertions. Formal Aspects of Computing, 6(Suppl 1):743\u2013765, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the International Cryptology Conference (Crypto)","author":"Bellare Mihir","year":"1996","unstructured":"Mihir Bellare, Ran Canetti, and Hugo Krawczyk. Keying hash functions for message authentication. In Proceedings of the International Cryptology Conference (Crypto), 1996."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Bornholt James","year":"2021","unstructured":"James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. Using lightweight formal methods to validate a key-value storage node in Amazon S3. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2021."},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the ACM International Conference on Very Large Databases (VLDB)","author":"Cao Wei","year":"2018","unstructured":"Wei Cao, Zhenjun Liu, Peng Wang, Sen Chen, Caifeng Zhu, Song Zheng, Yuhui Wang, and Guoqing Ma. PolarFS: An ultra-low latency and failure resilient distributed file system for shared storage cloud database. In Proceedings of the ACM International Conference on Very Large Databases (VLDB), 2018."},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Castro Miguel","year":"1999","unstructured":"Miguel Castro and Barbara Liskov. Practical Byzantine fault tolerance. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 1999."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Chajed Tej","year":"2018","unstructured":"Tej Chajed, M. Frans Kaashoek, Butler W. Lampson, and Nickolai Zeldovich. Verifying concurrent software using movers in CSPEC. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2018."},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Chajed Tej","year":"2019","unstructured":"Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Argosy: Verifying layered storage systems with recovery refinement. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019."},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Chajed Tej","year":"2022","unstructured":"Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying the DaisyNFS concurrent and crashsafe file system with sequential reasoning. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2022."},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the ACM Symposium on Principles of Distributed Computing (PODC)","author":"Chandra Tushar Deepak","year":"2007","unstructured":"Tushar Deepak Chandra, Robert Griesemer, and Joshua Redstone. Paxos made live: An engineering perspective. In Proceedings of the ACM Symposium on Principles of Distributed Computing (PODC), 2007."},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE)","author":"Chen Haicheng","year":"2020","unstructured":"Haicheng Chen, Wensheng Dou, Dong Wang, and Feng Qin. CoFI: Consistency-guided fault injection for cloud systems. In Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE), 2020."},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Chen Haogang","year":"2017","unstructured":"Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Mert Ileri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying a high-performance crash-safe file system using a tree specification. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2017."},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Chen Haogang","year":"2015","unstructured":"Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using crash Hoare logic for certifying the FSCQ file system. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2015."},{"key":"e_1_3_2_1_17_1","unstructured":"The OCaml Community. OCaml programming language. https:\/\/ocaml.org\/."},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"de Lima Chehab Rafael Lourenco","year":"2021","unstructured":"Rafael Lourenco de Lima Chehab, Antonio Paolillo, Diogo Behrens, Ming Fu, Hermann H\u00e4rtig, and Haibo Chen. CLoF: A compositional lock framework for multi-level NUMA systems. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2021."},{"issue":"3","key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/0743-1066(88)90010-6","article-title":"Automatic mode inference for logic programs","volume":"5","author":"Debray Saumya K.","year":"1988","unstructured":"Saumya K. Debray and David S. Warren. Automatic mode inference for logic programs. The Journal of Logic Programming, 5(3):207\u2013229, 1988.","journal-title":"The Journal of Logic Programming"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"Dragoi Cezara","year":"2016","unstructured":"Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. PSync: A partially synchronous language for fault-tolerant distributed algorithms. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2016."},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI)","author":"Drakos Nikos","year":"1989","unstructured":"Nikos Drakos. Unrestricted and parallel execution of logic programs with dependency directed backtracking. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), 1989."},{"key":"e_1_3_2_1_22_1","unstructured":"eBay. NuRaft. https:\/\/github.com\/eBay\/NuRaft."},{"key":"e_1_3_2_1_23_1","unstructured":"etcd. etcd Raft. https:\/\/github.com\/etcd-io\/etcd."},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the International Conference on Software Language Engineering (SLE)","author":"Ferreira Jos\u00e9 Pedro","year":"2025","unstructured":"Jos\u00e9 Pedro Ferreira, Jo\u00e3o Bispo, and Susana Lima. Transpilejs, an intelligent framework for transpiling JavaScript to webassembly. In Proceedings of the International Conference on Software Language Engineering (SLE), 2025."},{"key":"e_1_3_2_1_25_1","volume-title":"Proceedings of the Symposium on the Foundations of Software Engineering (FSE)","author":"Gao Yu","year":"2018","unstructured":"Yu Gao, Wensheng Dou, Feng Qin, Chushu Gao, Dong Wang, Jun Wei, Ruirui Huang, Li Zhou, and Yongming Wu. An empirical study on crash recovery bugs in large-scale distributed systems. In Proceedings of the Symposium on the Foundations of Software Engineering (FSE), 2018."},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE)","author":"Gao Yu","year":"2023","unstructured":"Yu Gao, Wensheng Dou, Dong Wang, Wenhan Feng, Jun Wei, Hua Zhong, and Tao Huang. Coverage guided fault injection for cloud systems. In Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE), 2023."},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE)","author":"Gao Yu","year":"2022","unstructured":"Yu Gao, Dong Wang, Qianwang Dai, Wensheng Dou, and Jun Wei. Common data guided crash injection for cloud systems. In Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE), 2022."},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE)","author":"Grant Stewart","year":"2018","unstructured":"Stewart Grant, Hendrik Cech, and Ivan Beschastnikh. Inferring and asserting distributed system invariants. In Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE), 2018."},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2016."},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Gulwani Sumit","year":"2011","unstructured":"Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. Synthesis of loop-free programs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2011."},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the ACM Symposium on Cloud Computing (SoCC)","author":"Gunawi Haryadi S.","year":"2014","unstructured":"Haryadi S. Gunawi, Mingzhe Hao, Tanakorn Leesatapornwongsa, Tiratat Patana-anake, Thanh Do, Jeffry Adityatama, Kurnia J. Eliazar, Agung Laksono, Jeffrey F. Lukman, Vincentius Martin, and Anang D. Satria. What bugs live in the cloud? A study of 3000+ issues in cloud systems. In Proceedings of the ACM Symposium on Cloud Computing (SoCC), 2014."},{"key":"e_1_3_2_1_32_1","volume-title":"Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Hackett Finn","year":"2023","unstructured":"Finn Hackett, Shayan Hosseini, Renato Costa, Matthew Do, and Ivan Beschastnikh. Compiling distributed system models with PGo. In Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2023."},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE)","author":"Hackett Finn","year":"2023","unstructured":"Finn Hackett, Joshua Rowe, and Markus Alexander Kuppe. Understanding inconsistency in Azure Cosmos DB with TLA+. In Proceedings of the IEEE\/ACM International Conference on Software Engineering (ICSE), 2023."},{"key":"e_1_3_2_1_34_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), 2021."},{"key":"e_1_3_2_1_35_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, Chris 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_1_36_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), 2023."},{"key":"e_1_3_2_1_37_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 Lowell Roberts, Srinath T. V. Setty, and Brian Zill. IronFleet: Proving practical distributed systems correct. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2015."},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Ileri Atalay Mert","year":"2018","unstructured":"Atalay Mert Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Proving confidentiality in a file system using DiskSec. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2018."},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the USENIX Conference on Annual Technical Conference (ATC)","author":"Kim Beom Heyn","year":"2022","unstructured":"Beom Heyn Kim, Taesoo Kim, and David Lie. Modulo: Finding convergence failure bugs in distributed systems with divergence resync models. In Proceedings of the USENIX Conference on Annual Technical Conference (ATC), 2022."},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Klein Gerwin","year":"2009","unstructured":"Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2009."},{"key":"e_1_3_2_1_41_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Kotla Ramakrishna","year":"2012","unstructured":"Ramakrishna Kotla, Tom Rodeheffer, Indrajit Roy, Patrick Stuedi, and Benjamin Wester. Pasture: Secure offline data access using commodity trusted hardware. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2012."},{"key":"e_1_3_2_1_42_1","unstructured":"Leslie Lamport. Industrial use of TLA+. https:\/\/lamport.azurewebsites.net\/tla\/industrial-use.html."},{"key":"e_1_3_2_1_43_1","unstructured":"Leslie Lamport. TLC model checker. https:\/\/lamport.azurewebsites.net\/tla\/current-tools.pdf."},{"issue":"3","key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lamport Leslie","year":"1994","unstructured":"Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_2_1_45_1","volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers.","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. 2002."},{"key":"e_1_3_2_1_46_1","volume-title":"Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC)","author":"Lamport Leslie","year":"2009","unstructured":"Leslie Lamport. The PlusCal algorithm language. In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC), 2009."},{"key":"e_1_3_2_1_47_1","volume-title":"Proceedings of the International Conference on Distributed Computing (DISC)","author":"Lamport Leslie","year":"2011","unstructured":"Leslie Lamport. Byzantizing Paxos by refinement. In Proceedings of the International Conference on Distributed Computing (DISC), 2011."},{"key":"e_1_3_2_1_48_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","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, Jacob R. Lorch, Oded Padon, and Bryan Parno. Verus: A practical foundation for systems verification. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2024."},{"key":"e_1_3_2_1_49_1","volume-title":"Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286\u2013315","author":"Lattuada Andrea","year":"2023","unstructured":"Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286\u2013315, 2023."},{"key":"e_1_3_2_1_50_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"LeBlanc Hayley","year":"2025","unstructured":"Hayley LeBlanc, Jacob R. Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, and Vijay Chidambaram. PoWER never corrupts: Tool-agnostic verification of crash consistency and corruption detection. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2025."},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Leesatapornwongsa Tanakorn","year":"2014","unstructured":"Tanakorn Leesatapornwongsa, Mingzhe Hao, Pallavi Joshi, Jeffrey F. Lukman, and Haryadi S. Gunawi. SAMC: Semantic-Aware model checking for fast discovery of deep bugs in cloud systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2014."},{"key":"e_1_3_2_1_52_1","volume-title":"Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Leesatapornwongsa Tanakorn","year":"2016","unstructured":"Tanakorn Leesatapornwongsa, Jeffrey F. Lukman, Shan Lu, and Haryadi S. Gunawi. TaxDC: A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2016."},{"key":"e_1_3_2_1_53_1","volume-title":"Logic for Programming, Artificial Intelligence","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, 2010."},{"key":"e_1_3_2_1_54_1","volume-title":"Proceedings of the ACM on Programming Languages, 6(OOPSLA1):1\u201328","author":"Li Jialin","year":"2022","unstructured":"Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel. Linear types for large-scale systems verification. Proceedings of the ACM on Programming Languages, 6(OOPSLA1):1\u201328, 2022."},{"key":"e_1_3_2_1_55_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Li Jialin","year":"2017","unstructured":"Jialin Li, Ellis Michael, and Dan R. K. Ports. Eris: Coordination-free consistent transactions using in-network concurrency control. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2017."},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Li Jialin","year":"2016","unstructured":"Jialin Li, Ellis Michael, Naveen Kr Sharma, Adriana Szekeres, and Dan RK Ports. Just say NO to Paxos overhead: Replacing consensus with network ordering. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2016."},{"key":"e_1_3_2_1_57_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Li Jialin","year":"2020","unstructured":"Jialin Li, Jacob Nelson, Ellis Michael, Xin Jin, and Dan R. K. Ports. Pegasus: Tolerating skewed workloads in distributed storage with in-network coherence directories. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2020."},{"key":"e_1_3_2_1_58_1","volume-title":"Proceedings of the ACM European Conference on Computer Systems (EuroSys)","author":"Li Jiaxin","year":"2018","unstructured":"Jiaxin Li, Yuxi Chen, Haopeng Liu, Shan Lu, Yiming Zhang, Haryadi S. Gunawi, Xiaohui Gu, Xicheng Lu, and Dongsheng Li. PCatch: Automatically detecting performance cascading bugs in cloud systems. In Proceedings of the ACM European Conference on Computer Systems (EuroSys), 2018."},{"issue":"3","key":"e_1_3_2_1_59_1","article-title":"Performance bug analysis and detection for distributed storage and computing systems","volume":"19","author":"Li Jiaxin","year":"2023","unstructured":"Jiaxin Li, Yiming Zhang, Shan Lu, Haryadi S. Gunawi, Xiaohui Gu, Feng Huang, and Dongsheng Li. Performance bug analysis and detection for distributed storage and computing systems. ACM Transactions on Storage, 19(3), 2023.","journal-title":"ACM Transactions on Storage"},{"key":"e_1_3_2_1_60_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), 2023."},{"key":"e_1_3_2_1_61_1","volume-title":"Proceedings of the USENIX Conference on Annual Technical Conference (ATC)","author":"Liu Bingzhe","year":"2024","unstructured":"Bingzhe Liu, Gangmuk Lim, Ryan Beckett, and Philip Brighten Godfrey. Kivi: Verification for cluster management. In Proceedings of the USENIX Conference on Annual Technical Conference (ATC), 2024."},{"key":"e_1_3_2_1_62_1","volume-title":"Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Liu Haopeng","year":"2017","unstructured":"Haopeng Liu, Guangpu Li, Jeffrey F. Lukman, Jiaxin Li, Shan Lu, Haryadi S. Gunawi, and Chen Tian. DCatch: Automatically detecting distributed concurrency bugs in cloud systems. In Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2017."},{"key":"e_1_3_2_1_63_1","volume-title":"Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Liu Haopeng","year":"2018","unstructured":"Haopeng Liu, Xu Wang, Guangpu Li, Shan Lu, Feng Ye, and Chen Tian. FCatch: Automatically detecting time-of-fault bugs in cloud systems. In Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2018."},{"key":"e_1_3_2_1_64_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Lou Chang","year":"2020","unstructured":"Chang Lou, Peng Huang, and Scott Smith. Understanding, detecting and localizing partial failures in large system software. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020."},{"key":"e_1_3_2_1_65_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Lu Jie","year":"2019","unstructured":"Jie Lu, Chen Liu, Lian Li, Xiaobing Feng, Feng Tan, Jun Yang, and Liang You. CrashTuner: Detecting crash-recovery bugs in cloud systems via meta-info analysis. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2019."},{"key":"e_1_3_2_1_66_1","volume-title":"Proceedings of the ACM European Conference on Computer Systems (EuroSys)","author":"Lukman Jeffrey F.","year":"2019","unstructured":"Jeffrey F. Lukman, Huan Ke, Cesar A. Stuardo, Riza O. Suminto, Daniar Heri Kurniawan, Dikaimin Simon, Satria Priambada, Chen Tian, Feng Ye, Tanakorn Leesatapornwongsa, Aarti Gupta, Shan Lu, and Haryadi S. Gunawi. FlyMC: Highly scalable testing of complex inter-leavings in distributed systems. In Proceedings of the ACM European Conference on Computer Systems (EuroSys), 2019."},{"key":"e_1_3_2_1_67_1","volume-title":"Proceedings of the USENIX Conference on Annual Technical Conference (ATC)","author":"Ma Haojun","year":"2022","unstructured":"Haojun Ma, Hammad Ahmad, Aman Goel, Eli Goldweber, Jean-Baptiste Jeannin, Manos Kapritsos, and Baris Kasikci. Sift: Using refinement-guided automation to verify complex distributed systems. In Proceedings of the USENIX Conference on Annual Technical Conference (ATC), 2022."},{"key":"e_1_3_2_1_68_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Ma Haojun","year":"2019","unstructured":"Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A. Sakallah. I4: Incremental inference of inductive invariants for verification of distributed protocols. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2019."},{"key":"e_1_3_2_1_69_1","volume-title":"Proceedings of the ACM SIGOPS Workshop on Hot Topics in Operating Systems (HotOS)","author":"Ma Haojun","year":"2019","unstructured":"Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A. Sakallah. Towards automatic inference of inductive invariants. In Proceedings of the ACM SIGOPS Workshop on Hot Topics in Operating Systems (HotOS), 2019."},{"key":"e_1_3_2_1_70_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Moraru Iulian","year":"2013","unstructured":"Iulian Moraru, David G. Andersen, and Michael Kaminsky. There is more consensus in egalitarian parliaments. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2013."},{"key":"e_1_3_2_1_71_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Mu Shuai","year":"2016","unstructured":"Shuai Mu, Lamont Nelson, Wyatt Lloyd, and Jinyang Li. Consolidating concurrency control and consensus for commits under conflicts. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2016."},{"key":"e_1_3_2_1_72_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."},{"issue":"4","key":"e_1_3_2_1_73_1","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/2699417","article-title":"How Amazon Web Services uses formal methods","volume":"58","author":"Newcombe Chris","year":"2015","unstructured":"Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. How Amazon Web Services uses formal methods. Communications of the ACM, 58(4):66\u201373, 2015.","journal-title":"Communications of the ACM"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_75_1","volume-title":"Proceedings of the USENIX Conference on Annual Technical Conference (ATC)","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John K. Ousterhout. In search of an understandable consensus algorithm. In Proceedings of the USENIX Conference on Annual Technical Conference (ATC), 2014."},{"key":"e_1_3_2_1_76_1","volume-title":"Proceedings of the ACM on Programming Languages, 2(OOPSLA):160:1\u2013160:28","author":"Ozkan Burcu Kulahcioglu","year":"2018","unstructured":"Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, and Georg Weissenbacher. Randomized testing of distributed systems with probabilistic guarantees. Proceedings of the ACM on Programming Languages, 2(OOPSLA):160:1\u2013160:28, 2018."},{"key":"e_1_3_2_1_77_1","volume-title":"Proceedings of the ACM on Programming Languages, 3(OOPSLA):180:1\u2013180:29","author":"Ozkan Burcu Kulahcioglu","year":"2019","unstructured":"Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Simin Oraee. Trace aware random testing for distributed systems. Proceedings of the ACM on Programming Languages, 3(OOPSLA):180:1\u2013180:29, 2019."},{"key":"e_1_3_2_1_78_1","volume-title":"Proceedings of the ACM on Programming Languages, 1(OOPSLA):108:1\u2013108:31","author":"Padon Oded","year":"2017","unstructured":"Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. Paxos made EPR: decidable reasoning about distributed protocols. Proceedings of the ACM on Programming Languages, 1(OOPSLA):108:1\u2013108:31, 2017."},{"key":"e_1_3_2_1_79_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Padon Oded","year":"2016","unstructured":"Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: Safety verification by interactive generalization. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2016."},{"key":"e_1_3_2_1_80_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Pick Lauren","year":"2023","unstructured":"Lauren Pick, Ankush Desai, and Aarti Gupta. Psym: Efficient symbolic exploration of distributed systems. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2023."},{"key":"e_1_3_2_1_81_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Pirelli Solal","year":"2022","unstructured":"Solal Pirelli, Akvile Valentukonyte, Katerina J. Argyraki, and George Candea. Automated verification of network function binaries. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2022."},{"key":"e_1_3_2_1_82_1","unstructured":"Microsoft Research. TLA+ proof system. https:\/\/proofs.tlapl.us\/doc\/web\/content\/Home.html."},{"issue":"2","key":"e_1_3_2_1_83_1","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","article-title":"Classes of recursively enumerable sets and their decision problems","volume":"74","author":"Rice H. G.","year":"1953","unstructured":"H. G. Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74(2):358\u2013366, 1953.","journal-title":"Transactions of the American Mathematical Society"},{"key":"e_1_3_2_1_84_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Ryzhyk Leonid","year":"2017","unstructured":"Leonid Ryzhyk, Nikolaj S. Bj\u00f8rner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, and George Varghese. Correct by construction networks using stepwise refinement. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2017."},{"key":"e_1_3_2_1_85_1","volume-title":"Proceedings of the International Conference on Distributed Computing and Networking (ICDCN)","author":"Santos Nuno","year":"2012","unstructured":"Nuno Santos and Andr\u00e9 Schiper. Tuning Paxos for high-throughput with batching and pipelining. In Proceedings of the International Conference on Distributed Computing and Networking (ICDCN), 2012."},{"key":"e_1_3_2_1_86_1","volume-title":"Proceedings of the ACM International Conference on Very Large Databases (VLDB)","author":"Schvimer Judah","year":"2020","unstructured":"Judah Schvimer, A. Jesse Jiryu Davis, and Max Hirschhorn. eXtreme modelling in practice. In Proceedings of the ACM International Conference on Very Large Databases (VLDB), 2020."},{"key":"e_1_3_2_1_87_1","volume-title":"Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"Sergey Ilya","year":"2018","unstructured":"Ilya Sergey, James R. Wilcox, and Zachary Tatlock. Programming and proving with distributed protocols. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2018."},{"key":"e_1_3_2_1_88_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Sharma Upamanyu","year":"2023","unstructured":"Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Grove: A separation-logic library for verifying distributed systems. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2023."},{"key":"e_1_3_2_1_89_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. Nickel: A framework for design and verification of information flow control systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2018."},{"key":"e_1_3_2_1_90_1","volume-title":"Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Solar-Lezama Armando","year":"2006","unstructured":"Armando Solar-Lezama, Liviu Tancau, Rastislav Bod\u00edk, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2006."},{"key":"e_1_3_2_1_91_1","volume-title":"Proceedings of the ACM on Programming Languages, 4(OOPSLA):152:1\u2013152:31","author":"Sprenger Christoph","year":"2020","unstructured":"Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter M\u00fcller, Martin Clochard, and David A. Basin. Igloo: Soundly linking compositional refinement and separation logic for distributed system verification. Proceedings of the ACM on Programming Languages, 4(OOPSLA):152:1\u2013152:31, 2020."},{"key":"e_1_3_2_1_92_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), 2024."},{"key":"e_1_3_2_1_93_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Taube Marcelo","year":"2018","unstructured":"Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. Modularity for decidability of deductive verification with applications to distributed systems. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2018."},{"key":"e_1_3_2_1_94_1","unstructured":"The CloudLab Team. CloudLab. https:\/\/www.cloudlab.us\/."},{"key":"e_1_3_2_1_95_1","unstructured":"The Coq Team. The Coq proof assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_96_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Tennage Pasindu","year":"2023","unstructured":"Pasindu Tennage, Cristina Basescu, Lefteris Kokoris-Kogias, Ewa Syta, Philipp Jovanovic, Vero Estrada-Gali\u00f1anes, and Bryan Ford. QuePaxa: Escaping the tyranny of timeouts in consensus. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2023."},{"key":"e_1_3_2_1_97_1","volume-title":"Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"von Gleissenthall Klaus","year":"2019","unstructured":"Klaus von Gleissenthall, Rami G\u00f6khan Kici, Alexander Bakst, Deian Stefan, and Ranjit Jhala. Pretend Synchrony: Synchronous verification of asynchronous distributed programs. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019."},{"key":"e_1_3_2_1_98_1","volume-title":"Proceedings of the ACM European Conference on Computer Systems (EuroSys)","author":"Wang Dong","year":"2023","unstructured":"Dong Wang, Wensheng Dou, Yu Gao, Chenao Wu, Jun Wei, and Tao Huang. Model checking guided testing for distributed systems. In Proceedings of the ACM European Conference on Computer Systems (EuroSys), 2023."},{"key":"e_1_3_2_1_99_1","volume-title":"Proceedings of the ACM International Conference on Very Large Databases (VLDB)","author":"Whittaker Michael J.","year":"2021","unstructured":"Michael J. Whittaker, Ailidani Ailijiang, Aleksey Charapko, Murat Demirbas, Neil Giridharan, Joseph M. Hellerstein, Heidi Howard, Ion Stoica, and Adriana Szekeres. Scaling replicated state machines with compartmentalization. In Proceedings of the ACM International Conference on Very Large Databases (VLDB), 2021."},{"key":"e_1_3_2_1_100_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Wilcox James R.","year":"2015","unstructured":"James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. Verdi: A framework for implementing and formally verifying distributed systems. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2015."},{"key":"e_1_3_2_1_101_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Certified Programs and Proofs (CPP)","author":"Woos Doug","year":"2016","unstructured":"Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas E. Anderson. Planning for change in a formal verification of the Raft consensus protocol. In Proceedings of the ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), 2016."},{"key":"e_1_3_2_1_102_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), 2022."},{"key":"e_1_3_2_1_103_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_1_104_1","volume-title":"Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Yuan Xinhao","year":"2020","unstructured":"Xinhao Yuan and Junfeng Yang. Effective concurrency testing for distributed systems. In Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2020."},{"key":"e_1_3_2_1_105_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV)","author":"Yuan Xinhao","year":"2018","unstructured":"Xinhao Yuan, Junfeng Yang, and Ronghui Gu. Partial order aware concurrency sampling. In Proceedings of the International Conference on Computer-Aided Verification (CAV), 2018."},{"key":"e_1_3_2_1_106_1","volume-title":"Proceedings of the ACM International Conference on Very Large Databases (VLDB)","author":"Zhang Haoran","year":"2024","unstructured":"Haoran Zhang, Shuai Mu, Sebastian Angel, and Vincent Liu. CausalMesh: A causal cache for stateful serverless computing. In Proceedings of the ACM International Conference on Very Large Databases (VLDB), 2024."},{"key":"e_1_3_2_1_107_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Zhang Irene","year":"2015","unstructured":"Irene Zhang, Naveen Kr. Sharma, Adriana Szekeres, Arvind Krishnamurthy, and Dan R. K. Ports. Building consistent transactions with inconsistent replication. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2015."},{"key":"e_1_3_2_1_108_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Zhang Kaiyuan","year":"2020","unstructured":"Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang. Automated verification of customizable middle-box properties with Gravel. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020."},{"key":"e_1_3_2_1_109_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhang Tony Nuda","year":"2024","unstructured":"Tony Nuda Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, and Bryan Parno. Inductive invariants that spark joy: Using invariant taxonomies to streamline distributed protocol proofs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2024."},{"key":"e_1_3_2_1_110_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Zhang Tony Nuda","year":"2023","unstructured":"Tony Nuda Zhang, Upamanyu Sharma, and Manos Kapritsos. Performal: Formal verification of latency properties for distributed systems. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2023."},{"key":"e_1_3_2_1_111_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhang Tony Nuda","year":"2025","unstructured":"Tony Nuda Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos, and Bryan Parno. Basilisk: Using provenance invariants to automate proofs of undecidable protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2025."},{"key":"e_1_3_2_1_112_1","volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)","author":"Zou Mo","year":"2019","unstructured":"Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu, and Haibo Chen. Using concurrent relational logic with helpers for verifying the AtomFS file system. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2019."},{"key":"e_1_3_2_1_113_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zou Mo","year":"2024","unstructured":"Mo Zou, Dong Du, Mingkai Dong, and Haibo Chen. Using dynamically layered definite releases for verifying the RefFS file system. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2024."}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","location":"Lotte Hotel World Seoul Republic of Korea","acronym":"SOSP '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles"],"original-title":[],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:54:10Z","timestamp":1759323250000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731569.3764822"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,12]]},"references-count":113,"alternative-id":["10.1145\/3731569.3764822","10.1145\/3731569"],"URL":"https:\/\/doi.org\/10.1145\/3731569.3764822","relation":{},"subject":[],"published":{"date-parts":[[2025,10,12]]},"assertion":[{"value":"2025-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}