{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:16:37Z","timestamp":1771024597380,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":92,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,22]],"date-time":"2024-04-22T00:00:00Z","timestamp":1713744000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006374","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS 2145295, CNS 2130560"],"award-info":[{"award-number":["CNS 2145295, CNS 2130560"]}],"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"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,22]]},"DOI":"10.1145\/3627703.3650077","type":"proceedings-article","created":{"date-parts":[[2024,4,18]],"date-time":"2024-04-18T06:28:28Z","timestamp":1713421708000},"page":"736-753","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["SandTable: Scalable Distributed System Model Checking with Specification-Level State Exploration"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0590-1620","authenticated-orcid":false,"given":"Ruize","family":"Tang","sequence":"first","affiliation":[{"name":"SKL for Novel Soft. Tech., Nanjing University, Nanjing, 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\/0000-0001-8921-036X","authenticated-orcid":false,"given":"Yu","family":"Huang","sequence":"additional","affiliation":[{"name":"SKL for Novel Soft. Tech., Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8137-2203","authenticated-orcid":false,"given":"Yuyang","family":"Wei","sequence":"additional","affiliation":[{"name":"SKL for Novel Soft. Tech., Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7523-8759","authenticated-orcid":false,"given":"Lingzhi","family":"Ouyang","sequence":"additional","affiliation":[{"name":"SKL for Novel Soft. Tech., Nanjing University, Nanjing, China"}],"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, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2008. Apache ZooKeeper. https:\/\/zookeeper.apache.org\/"},{"key":"e_1_3_2_1_2_1","unstructured":"2012. ZooKeeper#1: Leader election never settles for a 5-node cluster. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-1419"},{"key":"e_1_3_2_1_3_1","unstructured":"2013. WRaft. https:\/\/github.com\/willemt\/raft"},{"key":"e_1_3_2_1_4_1","unstructured":"2016. An incorrect unit test in WRaft. https:\/\/github.com\/willemt\/raft\/blob\/e428eeb921a014192d1d703dd317f3f29f5916c5\/tests\/test_snapshotting.c#L498"},{"key":"e_1_3_2_1_5_1","unstructured":"2016. DaosRaft. https:\/\/github.com\/daos-stack\/raft"},{"key":"e_1_3_2_1_6_1","unstructured":"2016. Jepsen. https:\/\/jepsen.io\/"},{"key":"e_1_3_2_1_7_1","unstructured":"2016. PySyncObj. https:\/\/github.com\/bakwc\/PySyncObj"},{"key":"e_1_3_2_1_8_1","unstructured":"2016. RaftOS. https:\/\/github.com\/zhebrak\/raftos"},{"key":"e_1_3_2_1_9_1","unstructured":"2018. RedisRaft. https:\/\/github.com\/RedisLabs\/raft"},{"key":"e_1_3_2_1_10_1","unstructured":"2018. Transparent proxy support - The Linux Kernel documentation. https:\/\/docs.kernel.org\/networking\/tproxy.html"},{"key":"e_1_3_2_1_11_1","unstructured":"2018. Xraft. https:\/\/github.com\/xnnyygn\/xraft\/tree\/master\/xraft-core"},{"key":"e_1_3_2_1_12_1","unstructured":"2018. Xraft-KVStore. https:\/\/github.com\/xnnyygn\/xraft\/tree\/master\/xraft-kvstore"},{"key":"e_1_3_2_1_13_1","unstructured":"2019. FlyMC Technical Report. https:\/\/tinyurl.com\/flymc-technical-report"},{"key":"e_1_3_2_1_14_1","unstructured":"2020. A bug in Raft TLA+: bugfix: HandleAppendEntriesRequest. https:\/\/github.com\/ongardie\/ratt.tla\/pull\/6"},{"key":"e_1_3_2_1_15_1","unstructured":"2021. Bugs confirmed by DaosRaft. Personal communication."},{"key":"e_1_3_2_1_16_1","unstructured":"2021. Bugs confirmed by RedisRaft. https:\/\/github.com\/RedisLabs\/raft\/issues\/49"},{"key":"e_1_3_2_1_17_1","unstructured":"2021. WRaft bugs. https:\/\/github.com\/willemt\/raft\/pull\/118"},{"key":"e_1_3_2_1_18_1","unstructured":"2022. PySyncObj#1: Fix disconnection when connecting. https:\/\/github.com\/bakwc\/PySyncObj\/pull\/161"},{"key":"e_1_3_2_1_19_1","unstructured":"2022. PySyncObj#2: Raft commit index is not monotonic. https:\/\/github.com\/bakwc\/PySyncObj\/issues\/166"},{"key":"e_1_3_2_1_20_1","unstructured":"2022. PySyncObj#3 and #4: Raft match index is not monotonic. https:\/\/github.com\/bakwc\/PySyncObj\/issues\/167"},{"key":"e_1_3_2_1_21_1","unstructured":"2022. PySyncObj#5: Leader commits log entries of older terms. https:\/\/github.com\/bakwc\/PySyncObj\/issues\/169"},{"key":"e_1_3_2_1_22_1","unstructured":"2023. DaosRaft#1: Reject request vote if self is leader. https:\/\/github.com\/daos-stack\/raft\/pull\/69"},{"key":"e_1_3_2_1_23_1","unstructured":"2023. dlfcn(3) manual pages. https:\/\/man.openbsd.org\/dlopen.3#dlsym"},{"key":"e_1_3_2_1_24_1","unstructured":"2023. Docker. https:\/\/www.docker.com\/"},{"key":"e_1_3_2_1_25_1","unstructured":"2023. ld.bfd(1) manual pages. https:\/\/man.openbsd.org\/ld.bfd.1#version-script="},{"key":"e_1_3_2_1_26_1","unstructured":"2023. ld.so(1) manual pages. https:\/\/man.openbsd.org\/ld.so.1#LD_PRELOAD"},{"key":"e_1_3_2_1_27_1","unstructured":"2023. LXD. https:\/\/ubuntu.com\/lxd"},{"key":"e_1_3_2_1_28_1","unstructured":"2023. RaftOS#1: Raft match index is not monotonic. https:\/\/github.com\/zhebrak\/raftos\/issues\/25"},{"key":"e_1_3_2_1_29_1","unstructured":"2023. RaftOS#2: Log may be erased incorrectly. https:\/\/github.com\/zhebrak\/raftos\/issues\/26"},{"key":"e_1_3_2_1_30_1","unstructured":"2023. RaftOS#3: KeyError in handling append_entries_response message. https:\/\/github.com\/zhebrak\/raftos\/issues\/27"},{"key":"e_1_3_2_1_31_1","unstructured":"2023. RaftOS#4: Change in update commit index. https:\/\/github.com\/zhebrak\/raftos\/pull\/30"},{"key":"e_1_3_2_1_32_1","unstructured":"2023. TLC and TLA+ Toolbox. https:\/\/github.com\/tlaplus\/tlaplus"},{"key":"e_1_3_2_1_33_1","unstructured":"2023. Xraft-KV#1: Read operations do not satisfy linearizability. https:\/\/github.com\/xnnyygn\/xraft\/issues\/40"},{"key":"e_1_3_2_1_34_1","unstructured":"2023. Xraft#1: Two leaders with the same term. https:\/\/github.com\/xnnyygn\/xraft\/issues\/33"},{"key":"e_1_3_2_1_35_1","unstructured":"2023. Xraft#2: Xraft-kvstore does not satisfy linearizability. https:\/\/github.com\/xnnyygn\/xraft\/issues\/39"},{"key":"e_1_3_2_1_36_1","unstructured":"2023. ZooKeeper TLA+ specification. https:\/\/github.com\/apache\/zookeeper\/tree\/master\/zookeeper-specifications\/system-spec"},{"key":"e_1_3_2_1_37_1","unstructured":"2024. SandTable. https:\/\/github.com\/tangruize\/SandTable"},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data (SIGMOD'15)","author":"Alvaro Peter","unstructured":"Peter Alvaro, Joshua Rosen, and Joseph M. Hellerstein. 2015. Lineage-driven Fault Injection. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data (SIGMOD'15)."},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'02)","author":"Ball Thomas","unstructured":"Thomas Ball and Sriram K. Rajamani. 2002. The SLAM project: debugging system software via static analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'02)."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2016.60"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_44_1","volume-title":"Workshop.","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke and E. Allen Emerson. 1981. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Logic of Programs, Workshop."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"E. M. Clarke E. A. Emerson S. Jha and A. P. Sistla. 1998. Symmetry reductions in model checking. In Computer Aided Verification (CAV'98).","DOI":"10.1007\/BFb0028741"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.14778\/3397230.3397233"},{"key":"e_1_3_2_1_48_1","unstructured":"Ankush Desai. 2013. The P programming language. https:\/\/github.com\/p-org\/P"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462184"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00186"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_53_1","volume-title":"Combining Model Checking and Testing","author":"Godefroid Patrice","unstructured":"Patrice Godefroid and Koushik Sen. 2018. Combining Model Checking and Testing. Springer International Publishing."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613161"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS55811.2022.00018"},{"key":"e_1_3_2_1_57_1","volume-title":"8th USENIX Symposium on Networked Systems Design and Implementation (NSDI'11)","author":"Guerraoui Rachid","year":"2011","unstructured":"Rachid Guerraoui and Maysam Yabandeh. 2011. Model Checking a Networked System Without the Network. In 8th USENIX Symposium on Networked Systems Design and Implementation (NSDI'11)."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575695"},{"key":"e_1_3_2_1_60_1","volume-title":"Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI'23)","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. 2023. Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI'23)."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSD.2001.981759"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523444"},{"key":"e_1_3_2_1_65_1","volume-title":"ZooKeeper: Wait-free Coordination for Internet-scale Systems. In 2010 USENIX Annual Technical Conference (ATC'10)","author":"Hunt Patrick","year":"2010","unstructured":"Patrick Hunt, Mahadev Konar, Flavio P. Junqueira, and Benjamin Reed. 2010. ZooKeeper: Wait-free Coordination for Internet-scale Systems. In 2010 USENIX Annual Technical Conference (ATC'10)."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958223"},{"key":"e_1_3_2_1_67_1","volume-title":"4th USENIX Symposium on Networked Systems Design & Implementation (NSDI'07)","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 4th USENIX Symposium on Networked Systems Design & Implementation (NSDI'07)."},{"key":"e_1_3_2_1_68_1","volume-title":"Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07)","author":"Killian Charles Edwin","unstructured":"Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, and Amin M. Vahdat. 2007. Mace: language support for building distributed systems. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07)."},{"key":"e_1_3_2_1_69_1","volume-title":"Modulo: Finding Convergence Failure Bugs in Distributed Systems with Divergence Resync Models. In 2022 USENIX Annual Technical Conference (ATC'22)","author":"Kim Beom Heyn","year":"2022","unstructured":"Beom Heyn Kim, Taesoo Kim, and David Lie. 2022. Modulo: Finding Convergence Failure Bugs in Distributed Systems with Divergence Resync Models. In 2022 USENIX Annual Technical Conference (ATC'22)."},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_71_1","unstructured":"Leslie Lamport. 2019. TLA+ specification for Paxos. https:\/\/github.com\/tlaplus\/Examples\/blob\/master\/specifications\/PaxosHowToWinATuringAward\/Paxos.tla"},{"key":"e_1_3_2_1_72_1","unstructured":"Leslie Lamport. 2021. PlusCal Introduction. https:\/\/lamport.azurewebsites.net\/tla\/tutorial\/intro.html"},{"key":"e_1_3_2_1_73_1","unstructured":"Leslie Lamport. 2022. TLA+Home Page. https:\/\/lamport.azurewebsites.net\/tla\/tla.html"},{"key":"e_1_3_2_1_74_1","volume-title":"SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14)","author":"Leesatapornwongsa Tanakorn","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 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14)."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359645"},{"key":"e_1_3_2_1_76_1","volume-title":"Proceedings of the Fourteenth EuroSys Conference 2019 (EuroSys'19)","author":"Lukman Jeffrey F.","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 Fourteenth EuroSys Conference 2019 (EuroSys'19)."},{"key":"e_1_3_2_1_77_1","volume-title":"5th Symposium on Operating Systems Design and Implementation (OSDI'02)","author":"Musuvathi Madanlal","unstructured":"Madanlal Musuvathi, David Y.W. Park, Andy Chou, Dawson R. Engler, and David L. Dill. 2002. CMC: A Pragmatic Approach to Model Checking Real Code. In 5th Symposium on Operating Systems Design and Implementation (OSDI'02)."},{"key":"e_1_3_2_1_78_1","volume-title":"Finding and Reproducing Heisenbugs in Concurrent Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08)","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08)."},{"key":"e_1_3_2_1_79_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)."},{"key":"e_1_3_2_1_80_1","unstructured":"Diego Ongaro. 2014. Consensus: bridging theory and practice. Ph.D. Dissertation. Stanford University USA."},{"key":"e_1_3_2_1_81_1","unstructured":"Diego Ongaro. 2014. TLA+ specification for Raft. https:\/\/github.com\/ongardie\/raft.tla"},{"key":"e_1_3_2_1_82_1","volume-title":"2014 USENIX Annual Technical Conference (ATC'14)","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In 2014 USENIX Annual Technical Conference (ATC'14)."},{"key":"e_1_3_2_1_83_1","volume-title":"SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings (SETTA'23)","author":"Ouyang Lingzhi","year":"2023","unstructured":"Lingzhi Ouyang, Yu Huang, Binyu Huang, and Xiaoxing Ma. 2023. Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service. In Dependable Software Engineering. Theories, Tools, and Applications: 9th International Symposium, SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings (SETTA'23)."},{"key":"e_1_3_2_1_84_1","volume-title":"Proc. ACM Program. Lang. 2, POPL","author":"Sergey Ilya","year":"2017","unstructured":"Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2017. Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2, POPL (2017)."},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_2_1_86_1","volume-title":"Azure Cosmos DB: Pushing the frontier of globally distributed databases. https:\/\/azure.microsoft.com\/en-us\/blog\/azure-cosmos-db-pushing-the-frontier-of-globally-distributed-databases\/","author":"Shukla Dharma","year":"2018","unstructured":"Dharma Shukla. 2018. Azure Cosmos DB: Pushing the frontier of globally distributed databases. https:\/\/azure.microsoft.com\/en-us\/blog\/azure-cosmos-db-pushing-the-frontier-of-globally-distributed-databases\/"},{"key":"e_1_3_2_1_87_1","volume-title":"5th International Workshop on Systems Software Verification (SSV'10)","author":"Simsa Jiri","year":"2010","unstructured":"Jiri Simsa, Randy Bryant, and Garth Gibson. 2010. dBug: Systematic Evaluation of Distributed Systems. In 5th International Workshop on Systems Software Verification (SSV'10)."},{"key":"e_1_3_2_1_88_1","volume-title":"Automatic Reliability Testing For Cluster Management Controllers. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI'22)","author":"Sun Xudong","year":"2022","unstructured":"Xudong Sun, Wenqing Luo, Jiawei Tyler Gu, Aishwarya Ganesan, Ramnatthan Alagappan, Michael Gasch, Lalith Suresh, and Tianyin Xu. 2022. Automatic Reliability Testing For Cluster Management Controllers. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI'22)."},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3552326.3587442"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_91_1","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI'09)","author":"Yabandeh Maysam","year":"2009","unstructured":"Maysam Yabandeh, Nikola Knezevic, Dejan Kostic, and Viktor Kuncak. 2009. CrystalBall: predicting and preventing inconsistencies in deployed distributed systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI'09)."},{"key":"e_1_3_2_1_92_1","volume-title":"MODIST: Transparent Model Checking of Unmodified Distributed Systems. In 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI'09)","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 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI'09)."}],"event":{"name":"EuroSys '24: Nineteenth European Conference on Computer Systems","location":"Athens Greece","acronym":"EuroSys '24","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the Nineteenth European Conference on Computer Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3627703.3650077","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3627703.3650077","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T01:11:41Z","timestamp":1755825101000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3627703.3650077"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,22]]},"references-count":92,"alternative-id":["10.1145\/3627703.3650077","10.1145\/3627703"],"URL":"https:\/\/doi.org\/10.1145\/3627703.3650077","relation":{},"subject":[],"published":{"date-parts":[[2024,4,22]]},"assertion":[{"value":"2024-04-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}