{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T12:32:09Z","timestamp":1756384329325,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":86,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,27]],"date-time":"2023-01-27T00:00:00Z","timestamp":1674777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["RGPIN-2020-05203, RGPIN-2014-04870"],"award-info":[{"award-number":["RGPIN-2020-05203, RGPIN-2014-04870"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008536","name":"Amazon Web Services","doi-asserted-by":"publisher","award":["Amazon Research Award (2022)"],"award-info":[{"award-number":["Amazon Research Award (2022)"]}],"id":[{"id":"10.13039\/100008536","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,27]]},"DOI":"10.1145\/3575693.3575695","type":"proceedings-article","created":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T22:56:55Z","timestamp":1675119415000},"page":"159-175","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Compiling Distributed System Models with PGo"],"prefix":"10.1145","author":[{"given":"Finn","family":"Hackett","sequence":"first","affiliation":[{"name":"University of British Columbia, Canada"}]},{"given":"Shayan","family":"Hosseini","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]},{"given":"Renato","family":"Costa","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]},{"given":"Matthew","family":"Do","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]},{"given":"Ivan","family":"Beschastnikh","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]}],"member":"320","published-online":{"date-parts":[[2023,1,30]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Eric Allen David Chase Joe Hallett Victor Luchangco Jan-Willem Maessen Sukyoung Ryu Guy Steele and Sam Tobin-Hochstadt. 2007. The Fortress Language Specification. \t\t\t\t  Eric Allen David Chase Joe Hallett Victor Luchangco Jan-Willem Maessen Sukyoung Ryu Guy Steele and Sam Tobin-Hochstadt. 2007. The Fortress Language Specification."},{"key":"e_1_3_2_1_2_1","volume-title":"Schneider","author":"Alpern Bowen","year":"1987","unstructured":"Bowen Alpern and Fred B . Schneider . 1987 . Recognizing safety and liveness. Distributed Computing , 2, 3 (1987), 01 Sep, 117\u2013126. issn:1432-0452 Bowen Alpern and Fred B. Schneider. 1987. Recognizing safety and liveness. Distributed Computing, 2, 3 (1987), 01 Sep, 117\u2013126. issn:1432-0452"},{"key":"e_1_3_2_1_3_1","unstructured":"Phil Bagwell. 2001. Ideal hash trees. Ecole Polytechnique Federale de Lausanne. \t\t\t\t  Phil Bagwell. 2001. Ideal hash trees. Ecole Polytechnique Federale de Lausanne."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.126768"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3375633"},{"key":"e_1_3_2_1_6_1","unstructured":"Annette Bieniusa Marek Zawirski Nuno Pregui\u00e7a Marc Shapiro Carlos Baquero Valter Balegas and S\u00e9rgio Duarte. 2012. An optimized conflict-free replicated set. arXiv preprint arXiv:1210.3368. \t\t\t\t  Annette Bieniusa Marek Zawirski Nuno Pregui\u00e7a Marc Shapiro Carlos Baquero Valter Balegas and S\u00e9rgio Duarte. 2012. An optimized conflict-free replicated set. arXiv preprint arXiv:1210.3368."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_1_8_1","volume-title":"Roshi: A CRDT system for timestamped events.  https:\/\/developers.soundcloud.com\/blog\/roshi-a-crdt-system-for-timestamped-events","author":"Bourgon Peter","year":"2014","unstructured":"Peter Bourgon . 2014 . Roshi: A CRDT system for timestamped events. https:\/\/developers.soundcloud.com\/blog\/roshi-a-crdt-system-for-timestamped-events Peter Bourgon. 2014. Roshi: A CRDT system for timestamped events. https:\/\/developers.soundcloud.com\/blog\/roshi-a-crdt-system-for-timestamped-events"},{"volume-title":"Introduction to reliable and secure distributed programming","author":"Cachin Christian","key":"e_1_3_2_1_9_1","unstructured":"Christian Cachin , Rachid Guerraoui , and Lu\u00eds Rodrigues . 2011. Introduction to reliable and secure distributed programming . Springer Science & Business Media . Christian Cachin, Rachid Guerraoui, and Lu\u00eds Rodrigues. 2011. Introduction to reliable and secure distributed programming. Springer Science & Business Media."},{"volume-title":"Ninth International Workshop on High-Level Parallel Programming Models and Supportive Environments.. 52\u201360","author":"Callahan D.","key":"e_1_3_2_1_10_1","unstructured":"D. Callahan , B.L. Chamberlain , and H.P. Zima . 2004. The cascade high productivity language . In Ninth International Workshop on High-Level Parallel Programming Models and Supportive Environments.. 52\u201360 . D. Callahan, B.L. Chamberlain, and H.P. Zima. 2004. The cascade high productivity language. In Ninth International Workshop on High-Level Parallel Programming Models and Supportive Environments.. 52\u201360."},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the International Workshop on Coq for Programming Languages (CoqPL).","author":"Chajed Tej","year":"2020","unstructured":"Tej Chajed , Joseph Tassarotti , Frans M. Kaashoek , and Nickolai Zeldovich . 2020 . Verifying concurrent Go code in Coq with Goose . In Proceedings of the International Workshop on Coq for Programming Languages (CoqPL). Tej Chajed, Joseph Tassarotti, Frans M. Kaashoek, and Nickolai Zeldovich. 2020. Verifying concurrent Go code in Coq with Goose. In Proceedings of the International Workshop on Coq for Programming Languages (CoqPL)."},{"key":"e_1_3_2_1_12_1","volume-title":"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 . 2022 . Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning . In USENIX Symposium on Operating Systems Design and Implementation (OSDI). Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. In USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/226643.226647"},{"key":"e_1_3_2_1_14_1","series-title":"Lecture Notes in Computer Science, 142\u2013148. issn:0302-9743","volume-title":"International Joint Conference on Automated Reasoning (IJCAR)","author":"Chaudhuri Kaustuv","unstructured":"Kaustuv Chaudhuri , Damien Doligez , Leslie Lamport , and Stephan Merz . 2010. International Joint Conference on Automated Reasoning (IJCAR) . Lecture Notes in Computer Science, 142\u2013148. issn:0302-9743 Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. 2010. International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Computer Science, 142\u2013148. issn:0302-9743"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1807128.1807152"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737996"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3472883.3486983"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462184"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_2_1_22_1","unstructured":"etcd. 2021. etcd.  https:\/\/etcd.io\/ \t\t\t\t  etcd. 2021. etcd.  https:\/\/etcd.io\/"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2008.4630075"},{"key":"e_1_3_2_1_26_1","unstructured":"GitHub. 2018. October 21 post-incident analysis.  https:\/\/github.blog\/2018-10-30-oct21-post-incident-analysis \t\t\t\t  GitHub. 2018. October 21 post-incident analysis.  https:\/\/github.blog\/2018-10-30-oct21-post-incident-analysis"},{"key":"e_1_3_2_1_27_1","unstructured":"GitLab. 2017. Postmortem of database outage of January 31.  https:\/\/about.gitlab.com\/2017\/02\/10\/postmortem-of-database-outage-of-january-31\/ \t\t\t\t  GitLab. 2017. Postmortem of database outage of January 31.  https:\/\/about.gitlab.com\/2017\/02\/10\/postmortem-of-database-outage-of-january-31\/"},{"key":"e_1_3_2_1_28_1","unstructured":"Google. 2022. global: Elevated HTTP 500s errors for a small number of customers with load balancers on Traffic Director-managed backends.  https:\/\/status.cloud.google.com\/incidents\/LuGcJVjNTeC5Sb9pSJ9o \t\t\t\t  Google. 2022. global: Elevated HTTP 500s errors for a small number of customers with load balancers on Traffic Director-managed backends.  https:\/\/status.cloud.google.com\/incidents\/LuGcJVjNTeC5Sb9pSJ9o"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180199"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7430228"},{"key":"e_1_3_2_1_32_1","unstructured":"Finn Hackett Shayan Hosseini Renato Costa Matthew Do and Ivan Beschastnikh. 2022. PGo.  https:\/\/distcompiler.github.io\/ \t\t\t\t  Finn Hackett Shayan Hosseini Renato Costa Matthew Do and Ivan Beschastnikh. 2022. PGo.  https:\/\/distcompiler.github.io\/"},{"key":"e_1_3_2_1_33_1","unstructured":"Finn Hackett Shayan Hosseini Renato Costa Matthew Do and Ivan Beschastnikh. 2022. PGo.  https:\/\/github.com\/DistCompiler\/pgo \t\t\t\t  Finn Hackett Shayan Hosseini Renato Costa Matthew Do and Ivan Beschastnikh. 2022. PGo.  https:\/\/github.com\/DistCompiler\/pgo"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7430244"},{"key":"e_1_3_2_1_35_1","unstructured":"Finn Hackett Shayan Hosseini Renato Costa Matthew Do and Ivan Beschastnikh. 2022. PGo Benchmarks.  https:\/\/github.com\/DistCompiler\/pgo-artifact \t\t\t\t  Finn Hackett Shayan Hosseini Renato Costa Matthew Do and Ivan Beschastnikh. 2022. PGo Benchmarks.  https:\/\/github.com\/DistCompiler\/pgo-artifact"},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI).","author":"Hance Travis","year":"2021","unstructured":"Travis Hance , Marijn Heule , Ruben Martins , and Bryan Parno . 2021 . Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All . In Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI). Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_3_2_1_38_1","unstructured":"Chris Hawblitzel Jon Howell Manos Kapritsos Jacob R. Lorch Bryan Parno Michael L. Roberts Srinath Setty and Brian Zill. 2022. IronClad Commit at which IronKV Implementation was evaluated.  https:\/\/github.com\/microsoft\/Ironclad\/tree\/bcb296737df6541c9542ad4e35499b347992f238 \t\t\t\t  Chris Hawblitzel Jon Howell Manos Kapritsos Jacob R. Lorch Bryan Parno Michael L. Roberts Srinath Setty and Brian Zill. 2022. IronClad Commit at which IronKV Implementation was evaluated.  https:\/\/github.com\/microsoft\/Ironclad\/tree\/bcb296737df6541c9542ad4e35499b347992f238"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523444"},{"key":"e_1_3_2_1_40_1","unstructured":"Ben Johnson. [n. d.]. Benbjohnson\/immutable: Immutable collections for go.  https:\/\/github.com\/benbjohnson\/immutable \t\t\t\t  Ben Johnson. [n. d.]. Benbjohnson\/immutable: Immutable collections for go.  https:\/\/github.com\/benbjohnson\/immutable"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132749"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI).","author":"Killian Charles","year":"2007","unstructured":"Charles Killian , James W Anderson , Ranjit Jhala , and Amin Vahdat . 2007 . Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code . In Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI). Charles Killian, James W Anderson, Ranjit Jhala, and Amin Vahdat. 2007. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_1_44_1","article-title":"Proving the Correctness of Multiprocess Programs","volume":"3","author":"Lamport Leslie","year":"1977","unstructured":"Leslie Lamport . 1977 . Proving the Correctness of Multiprocess Programs . IEEE Trans. Softw. Eng. , 3 , 2 (1977), Mar, 125\u2013143. issn:0098-5589 Leslie Lamport. 1977. Proving the Correctness of Multiprocess Programs. IEEE Trans. Softw. Eng., 3, 2 (1977), Mar, 125\u2013143. issn:0098-5589","journal-title":"IEEE Trans. Softw. Eng."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_46_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA . isbn:032114306X Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA. isbn:032114306X"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_2"},{"volume-title":"International Conference on Dependable Systems and Networks (DSN).","author":"Lee K. H.","key":"e_1_3_2_1_48_1","unstructured":"K. H. Lee , N. Sumner , X. Zhang , and P. Eugster . 2011. Unified debugging of distributed systems with Recon . In International Conference on Dependable Systems and Networks (DSN). K. H. Lee, N. Sumner, X. Zhang, and P. Eugster. 2011. Unified debugging of distributed systems with Recon. In International Conference on Dependable Systems and Networks (DSN)."},{"volume-title":"SAMC: Semantic-aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In USENIX Symposium on Operating Systems Design and Implementation (OSDI).","author":"Leesatapornwongsa Tanakorn","key":"e_1_3_2_1_49_1","unstructured":"Tanakorn Leesatapornwongsa , Mingzhe Hao , Pallavi Joshi , Jeffrey F. Lukman , and Haryadi S. Gunawi . 2014 . SAMC: Semantic-aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In USENIX Symposium on Operating Systems Design and Implementation (OSDI). Tanakorn Leesatapornwongsa, Mingzhe Hao, Pallavi Joshi, Jeffrey F. Lukman, and Haryadi S. Gunawi. 2014. SAMC: Semantic-aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_1_50_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M","author":"Leino Rustan","year":"2010","unstructured":"Rustan Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M . Clarke and Andrei Voronkov (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 348\u2013370. isbn:978-3-642-17511-4 Rustan Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M. Clarke and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 348\u2013370. isbn:978-3-642-17511-4"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837622"},{"volume-title":"NASA Formal Methods (NFM)","author":"Liu Si","key":"e_1_3_2_1_52_1","unstructured":"Si Liu , Atul Sandur , Jos\u00e9 Meseguer , Peter Csaba \u00d6lveczky , and Qi Wang . 2020. Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs . In NASA Formal Methods (NFM) . Springer International , 22\u201340. isbn:978-3-030-55754-6 Si Liu, Atul Sandur, Jos\u00e9 Meseguer, Peter Csaba \u00d6lveczky, and Qi Wang. 2020. Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs. In NASA Formal Methods (NFM). Springer International, 22\u201340. isbn:978-3-030-55754-6"},{"key":"e_1_3_2_1_53_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Liu Xuezheng","year":"2008","unstructured":"Xuezheng Liu , Zhenyu Guo , Xi Wang , Feibo Chen , Xiaochen Lian , Jian Tang , Ming Wu , M. Frans Kaashoek , and Zheng Zhang . 2008 . D3S: Debugging Deployed Distributed Systems . In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI). Xuezheng Liu, Zhenyu Guo, Xi Wang, Feibo Chen, Xiaochen Lian, Jian Tang, Ming Wu, M. Frans Kaashoek, and Zheng Zhang. 2008. D3S: Debugging Deployed Distributed Systems. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_1_54_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Liu Xuezheng","year":"2007","unstructured":"Xuezheng Liu , Wei Lin , Aimin Pan , and Zheng Zhang . 2007 . WiDS Checker: Combating Bugs in Distributed Systems . In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI). Xuezheng Liu, Wei Lin, Aimin Pan, and Zheng Zhang. 2007. WiDS Checker: Combating Bugs in Distributed Systems. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507753"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446756"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3033273"},{"volume-title":"Proceedings of the European Conference on Computer Systems (EuroSys).","author":"Lukman Jeffrey F.","key":"e_1_3_2_1_58_1","unstructured":"Jeffrey F. Lukman , Huan Ke , Cesar A. Stuardo , Riza O. Suminto , Daniar H. Kurniawan , Dikaimin Simon , Satria Priambada , Chen Tian , Feng Ye , Tanakorn Leesatapornwongsa , Aarti Gupta , Shan Lu , and Haryadi S. Gunawi . 2019. FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems . In Proceedings of the European Conference on Computer Systems (EuroSys). Jeffrey F. Lukman, Huan Ke, Cesar A. Stuardo, Riza O. Suminto, Daniar H. Kurniawan, Dikaimin Simon, Satria Priambada, Chen Tian, Feng Ye, Tanakorn Leesatapornwongsa, Aarti Gupta, Shan Lu, and Haryadi S. Gunawi. 2019. FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems. In Proceedings of the European Conference on Computer Systems (EuroSys)."},{"key":"e_1_3_2_1_59_1","volume-title":"USENIX 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 . 2022 . Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems . In USENIX Annual Technical Conference (ATC). Haojun Ma, Hammad Ahmad, Aman Goel, Eli Goldweber, Jean-Baptiste Jeannin, Manos Kapritsos, and Baris Kasikci. 2022. Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems. In USENIX Annual Technical Conference (ATC)."},{"volume-title":"Proceedings of the ACM Symposium on Operating Systems Principles (SOSP).","author":"Ma Haojun","key":"e_1_3_2_1_60_1","unstructured":"Haojun Ma , Aman Goel , Jean-Baptiste Jeannin , Manos Kapritsos , Baris Kasikci , and Karem A. Sakallah . 2019. I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols . In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP). Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A. Sakallah. 2019. I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)."},{"key":"e_1_3_2_1_61_1","article-title":"Pivot Tracing: Dynamic Causal Monitoring for Distributed Systems","volume":"35","author":"Mace Jonathan","year":"2018","unstructured":"Jonathan Mace , Ryan Roelke , and Rodrigo Fonseca . 2018 . Pivot Tracing: Dynamic Causal Monitoring for Distributed Systems . ACM Trans. Comput. Syst. , 35 , 4 (2018), Article 11, Dec., 28 pages. issn:0734-2071 Jonathan Mace, Ryan Roelke, and Rodrigo Fonseca. 2018. Pivot Tracing: Dynamic Causal Monitoring for Distributed Systems. ACM Trans. Comput. Syst., 35, 4 (2018), Article 11, Dec., 28 pages. issn:0734-2071","journal-title":"ACM Trans. Comput. Syst."},{"key":"e_1_3_2_1_62_1","volume-title":"Summers","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller , Malte Schwerhoff , and Alexander J . Summers . 2016 . Viper : A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI), B. Jobstmann and K. R. M. Leino (Eds.) (LNCS , Vol. 9583). Springer-Verlag, 41\u2013 62 . Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI), B. Jobstmann and K. R. M. Leino (Eds.) (LNCS, Vol. 9583). Springer-Verlag, 41\u201362."},{"key":"e_1_3_2_1_63_1","unstructured":"Jonathan Nadal. [n. d.]. Building Distributed Systems With Stateright. https:\/\/www.stateright.rs\/ Accessed: 2022-10-27 \t\t\t\t  Jonathan Nadal. [n. d.]. Building Distributed Systems With Stateright. https:\/\/www.stateright.rs\/ Accessed: 2022-10-27"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_65_1","volume-title":"How Amazon Web Services Uses Formal Methods. Commun. ACM, 58, 4","author":"Newcombe Chris","year":"2015","unstructured":"Chris Newcombe , Tim Rath , Fan Zhang , Bogdan Munteanu , Marc Brooker , and Michael Deardeuff . 2015. How Amazon Web Services Uses Formal Methods. Commun. ACM, 58, 4 ( 2015 ), Mar, 66\u201373. Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. How Amazon Web Services Uses Formal Methods. Commun. ACM, 58, 4 (2015), Mar, 66\u201373."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28121474"},{"key":"e_1_3_2_1_67_1","unstructured":"Diego Ongaro. 2021. Raft TLA+ specification.  https:\/\/github.com\/ongardie\/raft.tla \t\t\t\t  Diego Ongaro. 2021. Raft TLA+ specification.  https:\/\/github.com\/ongardie\/raft.tla"},{"key":"e_1_3_2_1_68_1","volume-title":"USENIX Annual Technical Conference (ATC).","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John Ousterhout . 2014 . In Search of an Understandable Consensus Algorithm . In USENIX Annual Technical Conference (ATC). Diego Ongaro and John Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In USENIX Annual Technical Conference (ATC)."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_71_1","volume-title":"Constable","author":"Rahli Vincent","year":"2015","unstructured":"Vincent Rahli , David Guaspari , Mark Bickford , and Robert L . Constable . 2015 . Formal Specification, Verification , and Implementation of Fault-Tolerant Systems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci. Technol ., 72 (2015). Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable. 2015. Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 72 (2015)."},{"key":"e_1_3_2_1_72_1","volume-title":"Introducing Badger: A fast key-value store written purely in go.  https:\/\/dgraph.io\/blog\/post\/badger\/","author":"Jain Manish Rai","year":"2017","unstructured":"Manish Rai Jain . 2017 . Introducing Badger: A fast key-value store written purely in go. https:\/\/dgraph.io\/blog\/post\/badger\/ Manish Rai Jain. 2017. Introducing Badger: A fast key-value store written purely in go. https:\/\/dgraph.io\/blog\/post\/badger\/"},{"key":"e_1_3_2_1_73_1","unstructured":"Redis. 2022. Redis.  https:\/\/redis.io\/ \t\t\t\t  Redis. 2022. Redis.  https:\/\/redis.io\/"},{"key":"e_1_3_2_1_74_1","volume-title":"Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Reynolds Patrick","year":"2006","unstructured":"Patrick Reynolds , Charles Killian , Janet L. Wiener , Jeffrey C. Mogul , Mehul A. Shah , and Amin Vahdat . 2006 . Pip: Detecting the Unexpected in Distributed Systems . In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI). Patrick Reynolds, Charles Killian, Janet L. Wiener, Jeffrey C. Mogul, Mehul A. Shah, and Amin Vahdat. 2006. Pip: Detecting the Unexpected in Distributed Systems. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Ilya Sergey James R. Wilcox and Zachary Tatlock. 2017. Programming and proving with distributed protocols. \t\t\t\t  Ilya Sergey James R. Wilcox and Zachary Tatlock. 2017. Programming and proving with distributed protocols.","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_1_76_1","volume-title":"Proceedings of the 5th International Conference on Systems Software Verification (SSV).","author":"Simsa Jiri","year":"2010","unstructured":"Jiri Simsa , Randy Bryant , and Garth Gibson . 2010 . dBug: Systematic Evaluation of Distributed Systems . In Proceedings of the 5th International Conference on Systems Software Verification (SSV). Jiri Simsa, Randy Bryant, and Garth Gibson. 2010. dBug: Systematic Evaluation of Distributed Systems. In Proceedings of the 5th International Conference on Systems Software Verification (SSV)."},{"key":"e_1_3_2_1_77_1","volume-title":"Cloudflare outage on","author":"Strickx Tom","year":"2022","unstructured":"Tom Strickx and Jeremy Hartman . 2022. Cloudflare outage on June 21, 2022 . https:\/\/blog.cloudflare.com\/cloudflare-outage-on-june-21-2022\/ Tom Strickx and Jeremy Hartman. 2022. Cloudflare outage on June 21, 2022. https:\/\/blog.cloudflare.com\/cloudflare-outage-on-june-21-2022\/"},{"issue":"9","key":"e_1_3_2_1_78_1","first-page":"0","article-title":"The Coq Proof Assistant","volume":"8","author":"Development Team The Coq","year":"2019","unstructured":"The Coq Development Team . 2019 . The Coq Proof Assistant , Version 8 . 9 . 0 . https:\/\/web.archive.org\/web\/20190415015254\/https:\/\/zenodo.org\/record\/2554024 The Coq Development Team. 2019. The Coq Proof Assistant, Version 8.9.0. https:\/\/web.archive.org\/web\/20190415015254\/https:\/\/zenodo.org\/record\/2554024","journal-title":"Version"},{"key":"e_1_3_2_1_79_1","volume-title":"Verdi: a framework for implementing and formally verifying distributed systems. ACM SIGPLAN Notices, 50, 6","author":"Wilcox James R.","year":"2015","unstructured":"James R. Wilcox , Doug Woos , Pavel Panchekha , Zachary Tatlock , Xi Wang , Michael D. Ernst , and Thomas Anderson . 2015. Verdi: a framework for implementing and formally verifying distributed systems. ACM SIGPLAN Notices, 50, 6 ( 2015 ), Jun, 357\u2013368. issn:03621340 James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. ACM SIGPLAN Notices, 50, 6 (2015), Jun, 357\u2013368. issn:03621340"},{"key":"e_1_3_2_1_80_1","unstructured":"James R. Wilcox Doug Woos Pavel Panchekha Zachary Tatlock Xi Wang Michael D. Ernst and Thomas Anderson. 2022. verdi-raft commit at which Vard implementation was evaluated.  https:\/\/github.com\/uwplse\/verdi-raft\/tree\/ea99a7453c30a0c11b904b36a3b4862fad28abe1 \t\t\t\t  James R. Wilcox Doug Woos Pavel Panchekha Zachary Tatlock Xi Wang Michael D. Ernst and Thomas Anderson. 2022. verdi-raft commit at which Vard implementation was evaluated.  https:\/\/github.com\/uwplse\/verdi-raft\/tree\/ea99a7453c30a0c11b904b36a3b4862fad28abe1"},{"key":"e_1_3_2_1_81_1","volume-title":"Gobra: Modular Specification and Verification of Go Programs. In International Conference on Computer Aided Verification (CAV).","author":"Wolf Felix A.","year":"2021","unstructured":"Felix A. Wolf , Linard Arquint , Martin Clochard , Wytse Oortwijn , Jo\u00e3o C. Pereira , and Peter M\u00fcller . 2021 . Gobra: Modular Specification and Verification of Go Programs. In International Conference on Computer Aided Verification (CAV). Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, Jo\u00e3o C. Pereira, and Peter M\u00fcller. 2021. Gobra: Modular Specification and Verification of Go Programs. In International Conference on Computer Aided Verification (CAV)."},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1731060.1731062"},{"key":"e_1_3_2_1_83_1","volume-title":"Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI).","author":"Yang Junfeng","year":"2009","unstructured":"Junfeng Yang , Tisheng Chen , Ming Wu , Zhilei Xu , Xuezheng Liu , Haoxiang Lin , Mao Yang , Fan Long , Lintao Zhang , and Lidong Zhou . 2009 . MODIST: Transparent Model Checking of Unmodified Distributed Systems . In Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI). Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou. 2009. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In Proceedings of the USENIX Conference on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_1_84_1","volume-title":"Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In USENIX Symposium on Operating Systems Design and Implementation (OSDI).","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao , Runzhou Tao , Ronghui Gu , and Jason Nieh . 2022 . DuoAI: Fast , Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In USENIX Symposium on Operating Systems Design and Implementation (OSDI). Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_1_85_1","volume-title":"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 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 . 2021 . DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In USENIX Symposium on Operating Systems Design and Implementation (OSDI). Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483577"}],"event":{"name":"ASPLOS '23: 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2","sponsor":["SIGARCH ACM Special Interest Group on Computer Architecture","SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Vancouver BC Canada","acronym":"ASPLOS '23"},"container-title":["Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3575693.3575695","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3575693.3575695","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:52Z","timestamp":1750272232000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3575693.3575695"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,27]]},"references-count":86,"alternative-id":["10.1145\/3575693.3575695","10.1145\/3575693"],"URL":"https:\/\/doi.org\/10.1145\/3575693.3575695","relation":{},"subject":[],"published":{"date-parts":[[2023,1,27]]},"assertion":[{"value":"2023-01-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}