{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:34:41Z","timestamp":1791459281397,"version":"4.3.4"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"ISSTA","license":[{"start":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T00:00:00Z","timestamp":1750550400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/publication-rights-and-licensing-policy"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62302493, 62072444"],"award-info":[{"award-number":["62302493, 62072444"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Major Project of ISCAS","award":["ISCAS-ZD-202302"],"award-info":[{"award-number":["ISCAS-ZD-202302"]}]},{"name":"Basic Research Project of ISCAS","award":["ISCAS-JCZD-202403"],"award-info":[{"award-number":["ISCAS-JCZD-202403"]}]},{"name":"Youth Innovation Promotion Association at Chinese Academy of Sciences","award":["Y2022044"],"award-info":[{"award-number":["Y2022044"]}]},{"name":"Major Program (JD) of Hubei Province","award":["2023BAA018"],"award-info":[{"award-number":["2023BAA018"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2025,6,22]]},"abstract":"<jats:p>Recently, model checking guided testing (MCGT) approaches have been proposed to systematically test distributed systems. MCGT automatically generates test cases by traversing the entire verified abstract state space derived from a distributed system's formal specification, and it checks whether the target system behaves correctly during testing. Despite the effectiveness of MCGT, testing a distributed system with MCGT is often costly and can take weeks to complete. This inefficiency is exacerbated when distributed systems evolve, such as when new features are introduced or bugs are fixed. We must re-run the entire testing process for the evolved system to verify its correctness, rendering MCGT not only resource-intensive but also inefficient.<\/jats:p>\n                  <jats:p>\n                    To reduce the overhead of model checking guided testing during distributed system evolution, we propose\n                    <jats:italic toggle=\"yes\">i<\/jats:italic>\n                    Mocket, a novel model checking guided incremental testing approach for distributed systems. We first extract the changes from both the formal specification and system implementation. We then identify the affected states within the abstract state space and generate incremental test cases that specifically target these states, thereby avoiding redundant testing of unaffected states. We evaluate\n                    <jats:italic toggle=\"yes\">i<\/jats:italic>\n                    Mocket using 12 real-world change scenarios drawn from three popular distributed systems. The experimental results demonstrate that\n                    <jats:italic toggle=\"yes\">i<\/jats:italic>\n                    Mocket can reduce the number of test cases by an average of 74.83% and decrease testing time by 22.54% to 99.99%. This highlights its effectiveness in lowering testing costs for distributed systems.\n                  <\/jats:p>","DOI":"10.1145\/3728883","type":"journal-article","created":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T10:52:56Z","timestamp":1750589576000},"page":"297-319","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking Guided Incremental Testing for Distributed Systems"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-8312-6736","authenticated-orcid":false,"given":"Yu","family":"Gao","sequence":"first","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-1874-6608","authenticated-orcid":false,"given":"Dong","family":"Wang","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3323-0449","authenticated-orcid":false,"given":"Wensheng","family":"Dou","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9856-9723","authenticated-orcid":false,"given":"Wenhan","family":"Feng","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2956-2021","authenticated-orcid":false,"given":"Yu","family":"Liang","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-6448-9345","authenticated-orcid":false,"given":"Yuan","family":"Feng","sequence":"additional","affiliation":[{"name":"Wuhan Dameng Database, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8561-2481","authenticated-orcid":false,"given":"Jun","family":"Wei","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,22]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"2007. Apache HBase. Retrieved April 18 2021 from https:\/\/hbase.apache.org\/"},{"key":"e_1_3_1_3_2","unstructured":"2008. Apache Hadoop HDFS. Retrieved March 29 2021 from http:\/\/hadoop.apache.org\/docs\/current\/hadoop-projectdist\/hadoop-hdfs\/HdfsDesign.html"},{"key":"e_1_3_1_4_2","unstructured":"2010. Apache ZooKeeper. Retrieved June 14 2020 from https:\/\/zookeeper.apache.org\/"},{"key":"e_1_3_1_5_2","unstructured":"2010. The TLA+ Toolbox. Retrieved May 6 2022 from http:\/\/lamport.azurewebsites.net\/tla\/toolbox.html"},{"key":"e_1_3_1_6_2","unstructured":"2012. Leader election never settles for a 5-node cluster. Retrieved Oct 2 2022 from https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-1419"},{"key":"e_1_3_1_7_2","unstructured":"2013. Zookeeper fails to start because of inconsistent epoch. Retrieved Oct 2 2022 from https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-1653"},{"key":"e_1_3_1_8_2","unstructured":"2014. TLA+ specification for the Raft consensus algorithm. Retrieved May 6 2022 from https:\/\/github.com\/ongardie\/raft.tla"},{"key":"e_1_3_1_9_2","unstructured":"2016. TLA+ examples. Retrieved January 12 2025 from https:\/\/github.com\/tlaplus\/Examples"},{"key":"e_1_3_1_10_2","unstructured":"2017. Raft-java. Retrieved April 11 2022 from https:\/\/github.com\/wenweihu86\/raft-java"},{"key":"e_1_3_1_11_2","unstructured":"2017. Raft-java issue#3. Retrieved April 25 2022 from https:\/\/github.com\/wenweihu86\/raft-java\/issues\/3"},{"key":"e_1_3_1_12_2","unstructured":"2018. High-level TLA+ specifications for the five consistency levels offered by Azure Cosmos DB. Retrieved January 12 2025 from https:\/\/github.com\/Azure\/azure-cosmos-tla"},{"key":"e_1_3_1_13_2","unstructured":"2018. Kafka specification. Retrieved January 12 2025 from https:\/\/github.com\/hachikuji\/kafka-specification"},{"key":"e_1_3_1_14_2","unstructured":"2018. XRaft. Retrieved April 11 2022 from https:\/\/github.com\/xnnyygn\/xraft"},{"key":"e_1_3_1_15_2","unstructured":"2019. Fixing a MongoDB Replication Protocol Bug with TLA+. Retrieved October 8 2023 from https:\/\/www.youtube.com\/watch?v=x9zSynTfLDE"},{"key":"e_1_3_1_16_2","unstructured":"2019. Raft-java issue#19. Retrieved April 25 2022 from https:\/\/github.com\/wenweihu86\/raft-java\/issues\/19"},{"key":"e_1_3_1_17_2","unstructured":"2019. TLA+ at Microsoft: 16 Years in Production. Retrieved October 8 2023 from https:\/\/www.youtube.com\/watch?v=azx6cX-BlCs"},{"key":"e_1_3_1_18_2","unstructured":"2019. Using TLA+ for Fun and Profit in the Development of Elasticsearch. Retrieved October 8 2023 from https:\/\/www.youtube.com\/watch?v=qYDcbcOVurc"},{"key":"e_1_3_1_19_2","unstructured":"2021. BookKeeper replication protocol TLA+ specification. Retrieved January 12 2025 from https:\/\/github.com\/Vanlightly\/bookkeeper-tlaplus"},{"key":"e_1_3_1_20_2","unstructured":"2022. Committed txns may be improperly truncated if follower crashes right after updating currentEpoch but before persisting txns to disk. Retrieved Nov 8 2023 from https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4643"},{"key":"e_1_3_1_21_2","unstructured":"2022. Committed txns may still be lost if followers crash after replying ACK of NEWLEADER but before writing txns to disk. Retrieved Nov 8 2023 from https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4646"},{"key":"e_1_3_1_22_2","unstructured":"2022. TLA+ in TiDB. Retrieved October 8 2023 from https:\/\/github.com\/pingcap\/tla-plus"},{"key":"e_1_3_1_23_2","unstructured":"2022. Unnecessary system unavailability due to leader shutdown when follower sent ACK of PROPOSAL before sending ACK of NEWLEADER in log recovery. Retrieved Nov 8 2023 from https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-4685"},{"key":"e_1_3_1_24_2","unstructured":"2022. Xraft commit: Handle with canceled votes. Retrieved April 24 2022 from https:\/\/github.com\/xnnyygn\/xraft\/pull\/28\/commits\/a48000080b6590402fbf45dd1a06af001d558830"},{"key":"e_1_3_1_25_2","unstructured":"2022. Xraft issue: Duplicate vote response can make illegal leader without a quorum. Retrieved April 24 2022 from https:\/\/github.com\/xnnyygn\/xraft\/issues\/27"},{"key":"e_1_3_1_26_2","unstructured":"2022. Xraft issue: VotedFor is not stored when a node is candidate and receives an AppendEntriesRpc. Retrieved May 6 2022 from https:\/\/github.com\/xnnyygn\/xraft\/issues\/29"},{"key":"e_1_3_1_27_2","unstructured":"2023. The 10 biggest cloud outages of 2023 (so far). Retrieved Nov 28 2023 from https:\/\/www.crn.com\/news\/cloud\/the-10-biggest-cloud-outages-of-2023-so-far-"},{"key":"e_1_3_1_28_2","unstructured":"2023. ZooKeeper specifications. Retrieved January 12 2025 from https:\/\/github.com\/apache\/zookeeper\/tree\/master\/zookeeper-specifications"},{"key":"e_1_3_1_29_2","doi-asserted-by":"crossref","unstructured":"Basil Alkhatib Sreeharsha Udayashankar Sara Qunaibi Ahmed Alquraan Mohammed Alfatafta Wael Al-Manasrah Alex Depoutovitch and Samer Al-Kiswany. 2022. Partial Network Partitioning. ACM Transactions on Computer Systems (2022).","DOI":"10.1145\/3576192"},{"key":"e_1_3_1_30_2","unstructured":"Ahmed Alquraan Hatem Takruri Mohammed Alfatafta and Samer Al-Kiswany. 2018. An analysis of network-partitioning failures in cloud systems. In Proceedings of USENIX Symposium on Operating Systems Design and Implementation (OSDI). 51\u201368."},{"key":"e_1_3_1_31_2","doi-asserted-by":"crossref","unstructured":"Hamid Bagheri and Sam Malek. 2016. Titanium: e\ufb03cient analysis of evolving alloy specifications. In Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE). 27\u201338.","DOI":"10.1145\/2950290.2950337"},{"key":"e_1_3_1_32_2","unstructured":"Haicheng Chen Wensheng Dou Dong Wang and Feng Qin. 2020. CoFI: Consistency-guided fault injection for cloud systems. In Proceedings of IEEE\/ACM SIGSOFT International Conference on Automated Software Engineering (ASE)."},{"key":"e_1_3_1_33_2","doi-asserted-by":"crossref","unstructured":"Yufeng Chen. 2021. NodeSRT: A selective regression testing tool for Node.js application. In Proceedings of IEEE\/ACM International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). 126\u2013128.","DOI":"10.1109\/ICSE-Companion52605.2021.00055"},{"key":"e_1_3_1_34_2","unstructured":"Zhao Chen. 2020. The Practice on Developing the Distributed Consensus Algorithm. Peking University Press."},{"key":"e_1_3_1_35_2","doi-asserted-by":"crossref","unstructured":"Ting Dai Jingzhu He Xiaohui Gu and Shan Lu. 2018. Understanding real-world timeout problems in cloud server systems. In Proceedings of IEEE International Conference on Cloud Engineering (IC2E). 1\u201311.","DOI":"10.1109\/IC2E.2018.00022"},{"issue":"9","key":"e_1_3_1_36_2","first-page":"1346","article-title":"eXtreme modelling in practice","volume":"13","author":"Davis A Jesse Jiryu","year":"2020","unstructured":"A Jesse Jiryu Davis, Max Hirschhorn, and Judah Schvimer. 2020. eXtreme modelling in practice. Proceedings of International Conference on Very Large Data Bases (VLDB) 13, 9 (2020), 1346\u20131358.","journal-title":"Proceedings of International Conference on Very Large Data Bases (VLDB)"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1327452.1327492"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.31"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.87284"},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","unstructured":"Yu Gao Wensheng Dou Feng Qin Chushu Gao Dong Wang Jun Wei Ruirui Huang Li Zhou and Yongming Wu. 2018. An empirical study on crash recovery bugs in large-scale distributed systems. In Proceedings of ACM SIGSOFT Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESCE\/FSE). 539\u2013550.","DOI":"10.1145\/3236024.3236030"},{"key":"e_1_3_1_41_2","doi-asserted-by":"crossref","unstructured":"Yu Gao Wensheng Dou Dong Wang Wenhan Feng Jun Wei Hua Zhong and Tao Huang. 2023. Coverage guided fault injection for cloud systems. In Proceedings of IEEE\/ACM SIGSOFT International Conference on Software Engineering (ICSE). 2211\u20132223.","DOI":"10.1109\/ICSE48619.2023.00186"},{"key":"e_1_3_1_42_2","doi-asserted-by":"crossref","unstructured":"Reiko Heckel and Leonardo Mariani. 2005. Automatic conformance testing of web services. In Proceedings of the 8th International Conference Held as Part of the Joint European Conference on Theory and Practice of Software Conference on Fundamental Approaches to Software Engineering (FASE). 34\u201348.","DOI":"10.1007\/978-3-540-31984-9_4"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.14778\/3415478.3415535"},{"key":"e_1_3_1_44_2","doi-asserted-by":"crossref","unstructured":"Flavio P Junqueira Benjamin C Reed and Marco Serafini. 2011. Zab: High-performance broadcast for primary-backup systems. In Proceedings of IEEE\/IFIP International Conference on Dependable Systems & Networks (DSN). 245\u2013256.","DOI":"10.1109\/DSN.2011.5958223"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3057269"},{"key":"e_1_3_1_46_2","doi-asserted-by":"crossref","unstructured":"Devin Kester Martin Mwebesa and Jeremy S Bradbury. 2010. How good is static analysis at finding concurrency bugs?. In Proceedings of IEEE Working Conference on Source Code Analysis and Manipulation (SCAM). 115\u2013124.","DOI":"10.1109\/SCAM.2010.26"},{"key":"e_1_3_1_47_2","unstructured":"Beom Heyn Kim Taesoo Kim and David Lie. 2022. Modulo: Finding convergence failure bugs in distributed systems with divergence resync models. In Proceedings of USENIX Annual Technical Conference (ATC). 383\u2013398."},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_1_49_2","unstructured":"Leslie Lamport. 2002. Specifying systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley."},{"key":"e_1_3_1_50_2","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 Proceedings of USENIX Symposium on Operating Systems Design and Implementation (OSDI). 399\u2013414."},{"key":"e_1_3_1_51_2","doi-asserted-by":"crossref","unstructured":"Tanakorn Leesatapornwongsa Jeffrey F Lukman Shan Lu and Haryadi S Gunawi. 2016. TaxDC: A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In Proceedings of ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). 517\u2013530.","DOI":"10.1145\/2872362.2872374"},{"key":"e_1_3_1_52_2","doi-asserted-by":"crossref","unstructured":"Jiaxin Li Yuxi Chen Haopeng Liu Shan Lu Yiming Zhang Haryadi S Gunawi Xiaohui Gu Xicheng Lu and Dongsheng Li. 2018. PCatch: Automatically detecting performance cascading bugs in cloud systems. In Proceedings of European Conference on Computer Systems (EuroSys). 1\u201314.","DOI":"10.1145\/3190508.3190552"},{"key":"e_1_3_1_53_2","doi-asserted-by":"crossref","unstructured":"Jiaxin Li Yiming Zhang Shan Lu Haryadi S Gunawi Xiaohui Gu Feng Huang and Dongsheng Li. 2023. Performance bug analysis and detection for distributed storage and computing systems. ACM Transactions on Storage (TOS) (2023) 1\u201331.","DOI":"10.1145\/3580281"},{"key":"e_1_3_1_54_2","doi-asserted-by":"crossref","unstructured":"Yishuai Li Benjamin C Pierce and Steve Zdancewic. 2021. Model-based testing of networked applications. In Proceedings of ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA). 529\u2013539.","DOI":"10.1145\/3460319.3464798"},{"key":"e_1_3_1_55_2","doi-asserted-by":"crossref","unstructured":"Haopeng Liu Guangpu Li Jeffrey F Lukman Jiaxin Li Shan Lu Haryadi S Gunawi and Chen Tian. 2017. DCatch: Automatically detecting distributed concurrency bugs in cloud systems. In Proceedings of ACM SIGARCH-SIGPLANSIGOPS International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). 677\u2013691.","DOI":"10.1145\/3037697.3037735"},{"key":"e_1_3_1_56_2","doi-asserted-by":"crossref","unstructured":"Haopeng Liu Xu Wang Guangpu Li Shan Lu Feng Ye and Chen Tian. 2018. FCatch: Automatically detecting time-of-fault bugs in cloud systems. In Proceedings of ACM SIGARCH-SIGPLAN-SIGOPS International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). 419\u2013431.","DOI":"10.1145\/3173162.3177161"},{"key":"e_1_3_1_57_2","doi-asserted-by":"crossref","unstructured":"Zhenyue Long Zeliu Ao Guoquan Wu Wei Chen and Jun Wei. 2020. WebRTS: A dynamic regression test selection tool for java web applications. In Proceedings of IEEE International Conference on Software Maintenance and Evolution (ICSME). 822\u2013825.","DOI":"10.1109\/ICSME46990.2020.00102"},{"key":"e_1_3_1_58_2","doi-asserted-by":"crossref","unstructured":"Jie Lu Chen Liu Lian Li Xiaobing Feng Feng Tan Jun Yang and Liang You. 2019. CrashTuner: Detecting crash-recovery bugs in cloud systems via meta-info analysis. In Proceedings of ACM SIGOPS Symposium on Operating Systems Principles (SOSP). 114\u2013130.","DOI":"10.1145\/3341301.3359645"},{"key":"e_1_3_1_59_2","doi-asserted-by":"crossref","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 et al. 2019. FlyMC: Highly scalable testing of complex interleavings in distributed systems. In Proceedings of European Conference on Computer Systems (EuroSys). 1\u201316.","DOI":"10.1145\/3302424.3303986"},{"key":"e_1_3_1_60_2","doi-asserted-by":"crossref","unstructured":"Daniel Neider Rick Smetsers Frits Vaandrager and Harco Kuppens. 2019. Benchmarks for automata learning and conformance testing. 390\u2013416.","DOI":"10.1007\/978-3-030-22348-9_23"},{"key":"e_1_3_1_61_2","doi-asserted-by":"crossref","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) 66\u201373.","DOI":"10.1145\/2699417"},{"key":"e_1_3_1_62_2","unstructured":"Diego Ongaro and John Ousterhout. 2014. In search of an understandable consensus algorithm. In Proceedings of USENIX Annual Technical Conference (ATC). 305\u2013319."},{"key":"e_1_3_1_63_2","doi-asserted-by":"crossref","unstructured":"Lingzhi Ouyang Yu Huang Binyu Huang and Xiaoxing Ma. 2023. Leveraging TLA+ specifications to improve the reliability of the ZooKeeper coordination service. In Proceedings of International Symposium on Dependable Software Engineering: Theories Tools and Applications (SETTA). 189\u2013205.","DOI":"10.1007\/978-981-99-8664-4_11"},{"key":"e_1_3_1_64_2","unstructured":"Alexandre Petrenko Nina Yevtushenko Alexandre Lebedev and Anindya Das. 1993. Nondeterministic state machines in protocol conformance testing. In Proceedings of the IFIP TC6\/WG6.1 Sixth International Workshop on Protocol Test Systems VI. 363\u2013378."},{"key":"e_1_3_1_65_2","doi-asserted-by":"crossref","unstructured":"Xiaoxia Ren Barbara G Ryder Maximilian Stoerzer and Frank Tip. 2005. Chianti: A change impact analysis tool for Java programs. In Proceedings of international conference on Software engineering. 664\u2013665.","DOI":"10.1109\/ICSE.2005.1553643"},{"key":"e_1_3_1_66_2","unstructured":"Jiri Simsa Randy Bryant and Garth Gibson. 2010. dBug: Systematic evaluation of distributed systems. In Proceedings of International Workshop on Systems Software Verification (SSV)."},{"key":"e_1_3_1_67_2","doi-asserted-by":"crossref","unstructured":"Rebecca Taft Irfan Sharif Andrei Matei Nathan VanBenschoten Jordan Lewis Tobias Grieger Kai Niemi Andy Woods Anne Birzin Raphael Poss et al. 2020. Cockroachdb: The resilient geo-distributed SQL database. In Proceedings of ACM SIGMOD International Conference on Management of Data (SIGMOD). 1493\u20131509.","DOI":"10.1145\/3318464.3386134"},{"key":"e_1_3_1_68_2","doi-asserted-by":"crossref","unstructured":"Ruize Tang Xudong Sun Yu Huang Wei Yuyang Lingzhi Ouyang and Xiaoxing Ma. 2024. SandTable: Scalable distributed system model checking with specification level state exploration. In Proceedings of European Conference on Computer Systems (EuroSys).","DOI":"10.1145\/3627703.3650077"},{"key":"e_1_3_1_69_2","doi-asserted-by":"crossref","unstructured":"Dong Wang Wensheng Dou Yu Gao Chenao Wu Jun Wei and Tao Huang. 2023. Model checking guided testing for distributed systems. In Proceedings of European Conference on Computer Systems (EuroSys). 51\u201367.","DOI":"10.1145\/3552326.3587442"},{"key":"e_1_3_1_70_2","unstructured":"Maysam Yabandeh Nikola Knezevic Dejan Kostic and Viktor Kuncak. 2009. CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. In Proceedings of USENIX Symposium on Networked Systems Design and Implementation (NSDI). 229\u2013244."},{"issue":"1","key":"e_1_3_1_71_2","article-title":"Directed incremental symbolic execution","volume":"24","author":"Yang Guowei","year":"2014","unstructured":"Guowei Yang, Suzette Person, Neha Rungta, and Sarfraz Khurshid. 2014. Directed incremental symbolic execution. ACM Transactions on Software Engineering and Methodology (TOSEM) 24, 1, Article 3 (2014), 42 pages.","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"e_1_3_1_72_2","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 USENIX Symposium on Networked Systems Design and Implementation (NSDI). 213\u2013228."},{"key":"e_1_3_1_73_2","doi-asserted-by":"crossref","unstructured":"Qiuping Yi and Guowei Yang. 2022. Feedback-driven incremental symbolic execution. In Proceedings of IEEE International Symposium on Software Reliability Engineering (ISSRE). 505\u2013516.","DOI":"10.1109\/ISSRE55969.2022.00055"},{"key":"e_1_3_1_74_2","unstructured":"Matei Zaharia Mosharaf Chowdhury Tathagata Das Ankur Dave Justin Ma Murphy McCauly Michael J Franklin Scott Shenker and Ion Stoica. 2012. Resilient distributed datasets: A fault-tolerant abstraction for in-memory cluster computing. In Proceedings of USENIX Symposium on Networked Systems Design and Implementation (NSDI). 15\u201328."},{"key":"e_1_3_1_75_2","doi-asserted-by":"crossref","unstructured":"Yuqi Zhang Yu Huang Hengfeng Wei and Xiaoxing Ma. 2022. MET: Model checking-driven explorative testing of CRDT designs and implementations. arXiv preprint arXiv:2204.14129 (2022).","DOI":"10.1002\/smr.2555"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3728883","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T13:51:13Z","timestamp":1787493073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3728883"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,22]]},"references-count":74,"journal-issue":{"issue":"ISSTA","published-print":{"date-parts":[[2025,6,22]]}},"alternative-id":["10.1145\/3728883"],"URL":"https:\/\/doi.org\/10.1145\/3728883","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,22]]}}}