{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:10Z","timestamp":1776304930915,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":107,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T00:00:00Z","timestamp":1743292800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"CCF-Huawei Populus Grove Fund","award":["CCF-HuaweiFM202304"],"award-info":[{"award-number":["CCF-HuaweiFM202304"]}]},{"name":"Cooperation Fund of Huawei-NJU Next Generation Programming Innovation Lab","award":["YBN2019105178SW38"],"award-info":[{"award-number":["YBN2019105178SW38"]}]},{"DOI":"10.13039\/501100006374","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-2130560, CNS-2145295"],"award-info":[{"award-number":["CNS-2130560, CNS-2145295"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62025202, 62372222"],"award-info":[{"award-number":["62025202, 62372222"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"name":"VMware Research Gift"},{"name":"Postgraduate Research & Practice Innovation Program of Jiangsu Province","award":["KYCX24_0235"],"award-info":[{"award-number":["KYCX24_0235"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,30]]},"DOI":"10.1145\/3689031.3696069","type":"proceedings-article","created":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T06:25:20Z","timestamp":1742970320000},"page":"379-395","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Multi-Grained Specifications for Distributed System Model Checking and Verification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7523-8759","authenticated-orcid":false,"given":"Lingzhi","family":"Ouyang","sequence":"first","affiliation":[{"name":"SKL for Novel Soft. Tech., Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6734-0928","authenticated-orcid":false,"given":"Xudong","family":"Sun","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana-Champaign, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-0590-1620","authenticated-orcid":false,"given":"Ruize","family":"Tang","sequence":"additional","affiliation":[{"name":"SKL for Novel Soft. Tech., Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8921-036X","authenticated-orcid":false,"given":"Yu","family":"Huang","sequence":"additional","affiliation":[{"name":"SKL for Novel Soft. Tech., Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9170-6524","authenticated-orcid":false,"given":"Madhav","family":"Jivrajani","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana-Champaign, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7970-1384","authenticated-orcid":false,"given":"Xiaoxing","family":"Ma","sequence":"additional","affiliation":[{"name":"SKL for Novel Soft. Tech., Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4443-8170","authenticated-orcid":false,"given":"Tianyin","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana-Champaign, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,3,30]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Ephemeral node is never deleted if follower fails while reading the proposal packet. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-2355","year":"2016","unstructured":"ZOOKEEPER-2355. Ephemeral node is never deleted if follower fails while reading the proposal packet. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-2355, 2016."},{"key":"e_1_3_2_2_2_1","volume-title":"Large databases take a long time to regain a quorum. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-2678","year":"2017","unstructured":"ZOOKEEPER-2678. Large databases take a long time to regain a quorum. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-2678, 2017."},{"key":"e_1_3_2_2_3_1","volume-title":"Data inconsistency issue due to retaining database in leader election. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-2845","year":"2017","unstructured":"ZOOKEEPER-2845. Data inconsistency issue due to retaining database in leader election. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-2845, 2017."},{"key":"e_1_3_2_2_4_1","volume-title":"Assertion fails when follower's history is not in sync with the leader's initial history after leader receives its ACK for NEWLEADER. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3023","year":"2018","unstructured":"ZOOKEEPER-3023. Assertion fails when follower's history is not in sync with the leader's initial history after leader receives its ACK for NEWLEADER. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3023, 2018."},{"key":"e_1_3_2_2_5_1","volume-title":"Potential data inconsistency due to NEWLEADER packet being sent too early during SNAP sync. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3104","year":"2018","unstructured":"ZOOKEEPER-3104. Potential data inconsistency due to NEWLEADER packet being sent too early during SNAP sync. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3104, 2018."},{"key":"e_1_3_2_2_6_1","volume-title":"Data inconsistency when the leader crashes right after sending SNAP sync. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3642","year":"2019","unstructured":"ZOOKEEPER-3642. Data inconsistency when the leader crashes right after sending SNAP sync. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3642, 2019."},{"key":"e_1_3_2_2_7_1","volume-title":"Data inconsistency caused by DIFF sync uncommitted log. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3911","year":"2020","unstructured":"ZOOKEEPER-3911. Data inconsistency caused by DIFF sync uncommitted log. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3911, 2020."},{"key":"e_1_3_2_2_8_1","volume-title":"https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4394","author":"Learner","year":"2021","unstructured":"ZOOKEEPER-4394. Learner.syncWithLeader got NullPointerException. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4394, 2021."},{"key":"e_1_3_2_2_9_1","volume-title":"https:\/\/github.com\/Azure\/azurecosmos-tla","author":"Azure Cosmos","year":"2022","unstructured":"Azure Cosmos TLA+ specifications. https:\/\/github.com\/Azure\/azurecosmos-tla, 2022."},{"key":"e_1_3_2_2_10_1","volume-title":"https:\/\/github.com\/pingcap\/tla-plus","author":"Ti DB.","year":"2022","unstructured":"TLA+ in TiDB. https:\/\/github.com\/pingcap\/tla-plus, 2022."},{"key":"e_1_3_2_2_11_1","volume-title":"Ephemeral znode owned by closed session visible in 1 of 3 servers. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4541","year":"2022","unstructured":"ZOOKEEPER-4541. Ephemeral znode owned by closed session visible in 1 of 3 servers. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4541, 2022."},{"key":"e_1_3_2_2_12_1","volume-title":"Committed transactions are improperly truncated when follower crashes right after updating currentEpoch. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4643","year":"2022","unstructured":"ZOOKEEPER-4643. Committed transactions are improperly truncated when follower crashes right after updating currentEpoch. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4643, 2022."},{"key":"e_1_3_2_2_13_1","volume-title":"Transaction loss when followers crash after replying ACK of NEWLEADER before logging transactions to disk. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4646","year":"2022","unstructured":"ZOOKEEPER-4646. Transaction loss when followers crash after replying ACK of NEWLEADER before logging transactions to disk. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4646, 2022."},{"key":"e_1_3_2_2_14_1","volume-title":"https:\/\/github.com\/etcd-io\/raft\/pull\/113","author":"Trace","year":"2023","unstructured":"Trace validation for the Raft consensus algorithm in etcd implementation. https:\/\/github.com\/etcd-io\/raft\/pull\/113, 2023."},{"key":"e_1_3_2_2_15_1","volume-title":"Unnecessary system unavailability due to leader shutdown when follower sends ACK of PROPOSAL before ACK of NEWLEADER. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4685","year":"2023","unstructured":"ZOOKEEPER-4685. Unnecessary system unavailability due to leader shutdown when follower sends ACK of PROPOSAL before ACK of NEWLEADER. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4685, 2023."},{"key":"e_1_3_2_2_16_1","volume-title":"Follower shutdown() does not correctly shutdown SyncProcessor, which leads to data inconsistency. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4712","year":"2023","unstructured":"ZOOKEEPER-4712. Follower shutdown() does not correctly shutdown SyncProcessor, which leads to data inconsistency. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4712, 2023."},{"key":"e_1_3_2_2_17_1","volume-title":"https:\/\/zookeeper.apache.org\/","author":"Apache ZooKeeper","year":"2024","unstructured":"Apache ZooKeeper. https:\/\/zookeeper.apache.org\/, 2024."},{"key":"e_1_3_2_2_18_1","volume-title":"https:\/\/eclipse.dev\/aspectj\/","author":"Aspect J.","year":"2024","unstructured":"AspectJ. https:\/\/eclipse.dev\/aspectj\/, 2024."},{"key":"e_1_3_2_2_19_1","volume-title":"https:\/\/jepsen.io\/","author":"Jepsen","year":"2024","unstructured":"Jepsen. https:\/\/jepsen.io\/, 2024."},{"key":"e_1_3_2_2_20_1","volume-title":"https:\/\/github.com\/microsoft\/CCF\/tree\/b10483af676354e21c19432099fcf43bdb6201ee\/tla","author":"Microsoft","year":"2024","unstructured":"Microsoft CCF TLA+ Specifications. https:\/\/github.com\/microsoft\/CCF\/tree\/b10483af676354e21c19432099fcf43bdb6201ee\/tla, 2024."},{"key":"e_1_3_2_2_21_1","volume-title":"https:\/\/github.com\/mongodb\/mongo\/tree\/r7.3.2\/src\/mongo\/tla_plus","author":"Mongo","year":"2024","unstructured":"MongoDB TLA+\/PlusCal Specifications. https:\/\/github.com\/mongodb\/mongo\/tree\/r7.3.2\/src\/mongo\/tla_plus, 2024."},{"key":"e_1_3_2_2_22_1","volume-title":"https:\/\/altsysrq.github.io\/proptest-book\/","author":"Proptest","year":"2024","unstructured":"Proptest documentation. https:\/\/altsysrq.github.io\/proptest-book\/, 2024."},{"key":"e_1_3_2_2_23_1","volume-title":"https:\/\/docs.oracle.com\/javase\/8\/docs\/technotes\/guides\/rmi\/index.html","author":"The Java Remote Method","year":"2024","unstructured":"The Java Remote Method Invocation API (Java RMI). https:\/\/docs.oracle.com\/javase\/8\/docs\/technotes\/guides\/rmi\/index.html, 2024."},{"key":"e_1_3_2_2_24_1","volume-title":"https:\/\/github.com\/etcd-io\/raft\/tree\/9ee2dd30d6a67a64a62ec8258bb33316c6f60283\/tla","author":"Specification","year":"2024","unstructured":"TLA+ Specification for etcd Raft. https:\/\/github.com\/etcd-io\/raft\/tree\/9ee2dd30d6a67a64a62ec8258bb33316c6f60283\/tla, 2024."},{"key":"e_1_3_2_2_25_1","volume-title":"https:\/\/github.com\/tlaplus\/tlaplus","author":"Toolbox","year":"2024","unstructured":"TLC and TLA+ Toolbox. https:\/\/github.com\/tlaplus\/tlaplus, 2024."},{"key":"e_1_3_2_2_26_1","volume-title":"Transaction loss due to race condition in Learner.syncWithLeader() during DIFF sync. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4785","year":"2024","unstructured":"ZOOKEEPER-4785. Transaction loss due to race condition in Learner.syncWithLeader() during DIFF sync. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4785, 2024."},{"key":"e_1_3_2_2_27_1","volume-title":"https:\/\/zookeeper.apache.org\/doc\/r3.9.1\/zookeeperUseCases.html","author":"ZooKeeper Use Cases","year":"2024","unstructured":"ZooKeeper Use Cases. https:\/\/zookeeper.apache.org\/doc\/r3.9.1\/zookeeperUseCases.html, 2024."},{"key":"e_1_3_2_2_28_1","volume-title":"https:\/\/github.com\/apache\/zookeeper\/blob\/release-3.9.1\/zookeeper-server\/src\/main\/java\/org\/apache\/zookeeper\/server\/quorum\/Learner.java","author":"ZooKeeper's","year":"2024","unstructured":"ZooKeeper's learner code. https:\/\/github.com\/apache\/zookeeper\/blob\/release-3.9.1\/zookeeper-server\/src\/main\/java\/org\/apache\/zookeeper\/server\/quorum\/Learner.java, 2024."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151647"},{"key":"e_1_3_2_2_30_1","first-page":"3","volume":"17","author":"Abadi M.","year":"1995","unstructured":"Abadi, M., and Lamport, L. Conjoining Specifications. ACM Transactions on Programming Languages and Systems 17, 3 (May 1995), 507--535.","journal-title":"Conjoining Specifications. ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_2_2_31_1","volume-title":"TLA+ Conference (Apr.","author":"Agrawal A.","year":"2024","unstructured":"Agrawal, A., and Policzer, Z. TLA+ @ LinkedIn: Ambry & Venice. In TLA+ Conference (Apr. 2024). https:\/\/youtu.be\/Jz0J5N77QKk."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354228"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2723372.2723711"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2016.60"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_2_36_1","volume-title":"TLA+ Conference (Apr.","author":"Brooker M.","year":"2024","unstructured":"Brooker, M. Fifteen Years of Formal Methods at AWS. In TLA+ Conference (Apr. 2024). https:\/\/youtu.be\/HxP4wi4DhA0."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416548"},{"key":"e_1_3_2_2_38_1","volume-title":"Proceedings of the 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI'23)","author":"Chen Y.","year":"2023","unstructured":"Chen, Y., Sun, X., Nath, S., Yang, Z., and Xu, T. \"Push-Button Reliability Testing for Cloud-Backed Applications with Rainmaker\". In Proceedings of the 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI'23) (Apr. 2023)."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359655"},{"key":"e_1_3_2_2_40_1","volume-title":"Validating Traces of Distributed Programs Against TLA+ Specifications. arXiv:2404.16075 (Apr","author":"Cirstea H.","year":"2024","unstructured":"Cirstea, H., Kuppe, M. A., Loillier, B., and Merz, S. Validating Traces of Distributed Programs Against TLA+ Specifications. arXiv:2404.16075 (Apr. 2024)."},{"key":"e_1_3_2_2_41_1","volume-title":"K. L. Compositional Model Checking. In Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS'89)","author":"Clarke E. M.","year":"1989","unstructured":"Clarke, E. M., Long, D. E., and McMillan, K. L. Compositional Model Checking. In Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS'89) (June 1989)."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.14778\/3397230.3397233"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462184"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065015"},{"key":"e_1_3_2_2_45_1","volume-title":"Proceedings of the 15th USENIX Conference on File and Storage Technologies (FAST'17)","author":"Ganesan A.","year":"2018","unstructured":"Ganesan, A., Alagappan, R., Arpaci-Dusseau, A. C., and Arpaci-Dusseau, R. H. Redundancy Does Not Imply Fault Tolerance: Analysis of Distributed Storage Reactions to Single Errors and Corruptions. In Proceedings of the 15th USENIX Conference on File and Storage Technologies (FAST'17) (Feb. 2018)."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613161"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS55811.2022.00018"},{"key":"e_1_3_2_2_48_1","volume-title":"Proceedings of the 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI'11)","author":"Guerraoui R.","year":"2011","unstructured":"Guerraoui, R., and Yabandeh, M. Model Checking a Networked System Without the Network. In Proceedings of the 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI'11) (Mar. 2011)."},{"key":"e_1_3_2_2_49_1","volume-title":"Proceedings of the 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI'11)","author":"Gunawi H. S.","year":"2011","unstructured":"Gunawi, H. S., Do, T., Joshi, P., Alvaro, P., Hellerstein, J. M., Arpaci-Dusseau, A. C., Arpaci-Dusseau, R. H., Sen, K., and Borthakur, D. Fate and Destini: A Framework for Cloud Recovery Testing. In Proceedings of the 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI'11) (Mar. 2011)."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575695"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-SEIP58684.2023.00006"},{"key":"e_1_3_2_2_53_1","volume-title":"Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI'21)","author":"Hance T.","year":"2021","unstructured":"Hance, T., Heule, M., Martins, R., and Parno, B. Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. In Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI'21) (Apr. 2021)."},{"key":"e_1_3_2_2_54_1","first-page":"366","volume":"2","author":"Havelund K.","year":"2000","unstructured":"Havelund, K., and Pressburger, T. Model Checking Java Programs Using Java PathFinder. International Journal on Software Tools for Technology Transfer 2 (2000), 366--381.","journal-title":"Model Checking Java Programs Using Java PathFinder. International Journal on Software Tools for Technology Transfer"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_2_56_1","volume-title":"Proceedings of the 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI'11)","author":"Hindman B.","year":"2011","unstructured":"Hindman, B., Konwinski, A., Zaharia, M., Ghodsi, A., Joseph, A. D., Katz, R., Shenker, S., and Stoica, I. Mesos: A Platform for Fine-Grained Resource Sharing in the Data Center. In Proceedings of the 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI'11) (Mar. 2011)."},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485474"},{"key":"e_1_3_2_2_58_1","volume-title":"Proceedings of the 2010 USENIX Annual Technical Conference (USENIX ATC'10) (June","author":"Hunt P.","year":"2010","unstructured":"Hunt, P., Konar, M., Junqueira, F. P., and Reed, B. ZooKeeper: Wait-Free Coordination for Internet-Scale Systems. In Proceedings of the 2010 USENIX Annual Technical Conference (USENIX ATC'10) (June 2010)."},{"key":"e_1_3_2_2_59_1","first-page":"2","volume":"16","author":"Jonsson","year":"1994","unstructured":"Jonsson, B. Compositional Specification and Verification of Distributed Systems. ACM Transactions on Programming Languages and Systems 16, 2 (Mar. 1994), 259--303.","journal-title":"Compositional Specification and Verification of Distributed Systems. ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_2_2_60_1","unstructured":"Junqueira F. P. Reed B. C. and Serafini M. Dissecting Zab. Tech. Rep. YL-2010-007 Yahoo! Research Dec. 2010."},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958223"},{"key":"e_1_3_2_2_62_1","volume-title":"Proceedings of the 4th USENIX Symposium on Networked Systems Design and Implementation (NSDI'07)","author":"Killian C.","year":"2007","unstructured":"Killian, C., Anderson, J. W., Jhala, R., and Vahdat, A. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In Proceedings of the 4th USENIX Symposium on Networked Systems Design and Implementation (NSDI'07) (Apr. 2007)."},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_3_2_2_64_1","volume-title":"Proceedings of the 2022 USENIX Annual Technical Conference (ATC'22)","author":"Kim B. H.","year":"2022","unstructured":"Kim, B. H., Kim, T., and Lie, D. Modulo: Finding Convergence Failure Bugs in Distributed Systems with Divergence Resync Models. In Proceedings of the 2022 USENIX Annual Technical Conference (ATC'22) (July 2022)."},{"key":"e_1_3_2_2_65_1","volume-title":"TLA+ Conference (Apr.","author":"Kuppe M. A.","year":"2024","unstructured":"Kuppe, M. A. Validating System Executions with the TLA+ Tools. In TLA+ Conference (Apr. 2024). https:\/\/youtu.be\/NZmON-XmrkI."},{"key":"e_1_3_2_2_66_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","year":"2002","unstructured":"Lamport, L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Aug. 2002."},{"key":"e_1_3_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.88"},{"key":"e_1_3_2_2_69_1","volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI'14)","author":"Leesatapornwongsa T.","year":"2014","unstructured":"Leesatapornwongsa, T., Hao, M., Joshi, P., Lukman, J. F., and Gunawi, H. S. SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI'14) (Oct. 2014)."},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872374"},{"key":"e_1_3_2_2_71_1","volume-title":"K. R. M. Dafny: An Automatic Program Verifier for Functional Correctness. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10)","author":"Leino","year":"2010","unstructured":"Leino, K. R. M. Dafny: An Automatic Program Verifier for Functional Correctness. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10) (Apr. 2010)."},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037735"},{"key":"e_1_3_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177161"},{"key":"e_1_3_2_2_74_1","volume-title":"TLA+ Conference (Apr.","author":"Loncaric C.","year":"2024","unstructured":"Loncaric, C. Reverse-Engineering with TLA+ at Oracle. In TLA+ Conference (Apr. 2024). https:\/\/youtu.be\/dGBSeagCAxw."},{"key":"e_1_3_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359645"},{"key":"e_1_3_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303986"},{"key":"e_1_3_2_2_77_1","volume-title":"Proceedings of the 2022 USENIX Annual Technical Conference (ATC'22)","author":"Ma H.","year":"2022","unstructured":"Ma, H., Ahmad, H., Goel, A., Goldweber, E., Jeannin, J.-B., Kapritsos, M., and Kasikci, B. Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems. In Proceedings of the 2022 USENIX Annual Technical Conference (ATC'22) (July 2022)."},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_3_2_2_79_1","volume-title":"Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17)","author":"Mari\u0107 O.","year":"2017","unstructured":"Mari\u0107, O., Sprenger, C., and Basin, D. Cutoff Bounds for Consensus Algorithms. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17) (July 2017)."},{"key":"e_1_3_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"e_1_3_2_2_81_1","first-page":"4","volume":"58","author":"Newcombe C.","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., and Deardeuff, M. How Amazon Web Services Uses Formal Methods. Communications of the ACM 58, 4 (Mar. 2015), 66--73.","journal-title":"How Amazon Web Services Uses Formal Methods. Communications of the ACM"},{"key":"e_1_3_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-99-8664-4_11"},{"key":"e_1_3_2_2_83_1","volume-title":"Multi-Grained Specifications for Distributed System Model Checking and Verification. arXiv:2409.14301 (Sept","author":"Ouyang L.","year":"2024","unstructured":"Ouyang, L., Sun, X., Tang, R., Huang, Y., Jivrajani, M., Ma, X., and Xu, T. Multi-Grained Specifications for Distributed System Model Checking and Verification. arXiv:2409.14301 (Sept. 2024)."},{"key":"e_1_3_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276530"},{"key":"e_1_3_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529974.1529978"},{"key":"e_1_3_2_2_87_1","volume-title":"May","author":"Reed B.","year":"2021","unstructured":"Reed, B., Junqueira, F. P., and Han, M. Zab1.0. https:\/\/cwiki.apache.org\/confluence\/display\/ZOOKEEPER\/Zab1.0, May 2021."},{"key":"e_1_3_2_2_88_1","volume-title":"Efficient Verification of Distributed Protocols Using Stateful Model Checking. In 2013 IEEE 32nd International Symposium on Reliable Distributed Systems (SRDS'13)","author":"Saissi H.","year":"2013","unstructured":"Saissi, H., Bokor, P., Muftuoglu, C. A., Suri, N., and Serafini, M. Efficient Verification of Distributed Protocols Using Stateful Model Checking. In 2013 IEEE 32nd International Symposium on Reliable Distributed Systems (SRDS'13) (Sept. 2013)."},{"key":"e_1_3_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_2_2_91_1","volume-title":"Proceedings of the 5th International Conference on Systems Software Verification (SSV'10)","author":"Simsa J.","year":"2010","unstructured":"Simsa, J., Bryant, R., and Gibson, G. dBug: Systematic Evaluation of Distributed Systems. In Proceedings of the 5th International Conference on Systems Software Verification (SSV'10) (Oct. 2010)."},{"key":"e_1_3_2_2_92_1","volume-title":"Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI'22)","author":"Sun X.","year":"2022","unstructured":"Sun, X., Luo, W., Gu, J. T., Ganesan, A., Alagappan, R., Gasch, M., Suresh, L., and Xu, T. Automatic Reliability Testing for Cluster Management Controllers. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI'22) (July 2022)."},{"key":"e_1_3_2_2_93_1","volume-title":"Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI'24)","author":"Sun X.","year":"2024","unstructured":"Sun, X., Ma, W., Gu, J. T., Ma, Z., Chajed, T., Howell, J., Lattuada, A., Padon, O., Suresh, L., Szekeres, A., and Xu, T. Anvil: Verifying Liveness of Cluster Management Controllers. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI'24) (July 2024)."},{"key":"e_1_3_2_2_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815401"},{"key":"e_1_3_2_2_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/3627703.3650077"},{"key":"e_1_3_2_2_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775926"},{"key":"e_1_3_2_2_97_1","first-page":"8","volume":"56","author":"Tseitlin","year":"2013","unstructured":"Tseitlin, A. The Antifragile Organization. Communications of the ACM 56, 8 (Aug. 2013), 40--44.","journal-title":"The Antifragile Organization. Communications of the ACM"},{"key":"e_1_3_2_2_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/3552326.3587442"},{"key":"e_1_3_2_2_99_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_2_100_1","doi-asserted-by":"publisher","DOI":"10.5555\/3691825.3691895"},{"key":"e_1_3_2_2_101_1","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI'09)","author":"Yabandeh M.","year":"2009","unstructured":"Yabandeh, M., Knezevic, N., Kostic, D., and Kuncak, V. CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI'09) (Apr. 2009)."},{"key":"e_1_3_2_2_102_1","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI'09)","author":"Yang J.","year":"2009","unstructured":"Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., and Zhou, L. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI'09) (Apr. 2009)."},{"key":"e_1_3_2_2_103_1","volume-title":"Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI '22)","author":"Yao J.","year":"2022","unstructured":"Yao, J., Tao, R., Gu, R., and Nieh, J. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI '22) (July 2022)."},{"key":"e_1_3_2_2_104_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632877"},{"key":"e_1_3_2_2_105_1","volume-title":"Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI'21)","author":"Yao J.","year":"2021","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., and Ryan, G. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI'21) (July 2021)."},{"key":"e_1_3_2_2_106_1","volume-title":"Proceedings of the 25th International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '20)","author":"Yuan X.","year":"2018","unstructured":"Yuan, X., and Yang, J. Effective Concurrency Testing for Distributed Systems. In Proceedings of the 25th International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '20) (Mar. 2018)."},{"key":"e_1_3_2_2_107_1","volume-title":"TLA+ Conference (Apr.","author":"Zhou S.","year":"2024","unstructured":"Zhou, S. How We Designed and Model-Checked MongoDB Reconfiguration Protocol. In TLA+ Conference (Apr. 2024). https:\/\/youtu.be\/-eAktIBUhHA."}],"event":{"name":"EuroSys '25: Twentieth European Conference on Computer Systems","location":"Rotterdam Netherlands","acronym":"EuroSys '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the Twentieth European Conference on Computer Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689031.3696069","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689031.3696069","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T11:25:25Z","timestamp":1755775525000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689031.3696069"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,30]]},"references-count":107,"alternative-id":["10.1145\/3689031.3696069","10.1145\/3689031"],"URL":"https:\/\/doi.org\/10.1145\/3689031.3696069","relation":{},"subject":[],"published":{"date-parts":[[2025,3,30]]},"assertion":[{"value":"2025-03-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}