Page 320 - 《软件学报》2026年第5期

唐瑞泽 等: 分布式系统模型检验技术研究进展 2199

do not terminate. In: Proc. of the 23rd Int’l Conf. Verification, Model Checking, and Abstract Interpretation. Philadelphia: Springer,
2022. 400–424. [doi: 10.1007/978-3-030-94583-1_20]
[100] Simsa J, Bryant R, Gibson G, Hickey J. Scalable dynamic partial order reduction. In: Qadeer S, Tasiran S, eds. Runtime Verification.
Berlin, Heidelberg: Springer, 2013. 19–34. [doi: 10.1007/978-3-642-35632-2_4]
[101] Abdulla PA, Aronis S, Jonsson B, Sagonas K. Source sets: A foundation for optimal dynamic partial order reduction. Journal of the
ACM (JACM), 2017, 64(4): 25. [doi: 10.1145/3073408]
[102] Godefroid P. Exploiting symmetry when model-checking software. In: Wu JP, Chanson ST, Gao Q, eds. Formal Methods for Protocol
Engineering and Distributed Systems. Boston: Springer, 1999. 257–275. [doi: 10.1007/978-0-387-35578-8_15]
[103] Kokologiannakis M, Marmanis I, Vafeiadis V. Spore: Combining symmetry and partial order reduction. Proc. of the ACM on
Programming Languages, 2024, 8(PLDI): 219. [doi: 10.1145/3656449]
[104] Lukman JF. FlyMC technical report. 2019. https://tinyurl.com/flymc-technicalreport
[105] Nethercote N, Seward J. Valgrind: A framework for heavyweight dynamic binary instrumentation. In: Proc. of the 28th ACM SIGPLAN
Conf. on Programming Language Design and Implementation. San Diego: ACM, 2007. 89–100. [doi: 10.1145/1250734.1250746]
[106] Clarke EM, Emerson EA, Jha S, Sistla AP. Symmetry reductions in model checking. In: Proc. of the 10th Int’l Conf. on Computer Aided
Verification. Vancouver: Springer, 1998. 147–158. [doi: 10.1007/BFb0028741]
[107] Gunawi HS, Do T, Joshi P, Alvaro P, Hellerstein JM, Arpaci-Dusseau AC, Arpaci-Dusseau RH, Sen K, Borthakur D. FATE and
DESTINI: A framework for cloud recovery testing. In: Proc. of the 8th USENIX Conf. on Networked Systems Design and
Implementation. Boston: USENIX Association, 2011. 238–252.
[108] Alvaro P, Rosen J, Hellerstein JM. Lineage-driven fault injection. In: Proc. of the 2015 ACM SIGMOD Int’l Conf. on Management of
Data. Melbourne: ACM, 2015. 331–346. [doi: 10.1145/2723372.2723711]
[109] Kim BH, Kim T, Lie D. Modulo: Finding convergence failure bugs in distributed systems with divergence resync models. In: Proc. of
the 2022 USENIX Annual Technical Conf. Carlsbad: USENIX Association, 2022. 383–398.
[110] Methni A, Lemerre M, Ben Hedia B, Haddad S, Barkaoui K. Specifying and verifying concurrent C programs with TLA+. In: Artho C,
Ölveczky PC, eds. Formal Techniques for Safety-critical Systems. Cham: Springer, 2015. 206–222. [doi: 10.1007/978-3-319-17581-
2_14]
[111] Corbett JC, Dwyer MB, Hatcliff J, Laubach S, Păsăreanu CS, Robby, Zheng HJ. Bandera: Extracting finite-state models from Java
source code. In: Proc. of the 22nd Int’l Conf. on Software Engineering. Limerick: ACM, 2000. 439–448. [doi: 10.1145/337180.337234]
[112] Havelund K. Java PathFinder a translator from Java to Promela. In: Dams D, Gerth R, Leue S, Massink M, eds. Theoretical and Practical
Aspects of SPIN Model Checking. Berlin: Springer, 1999. 152. [doi: 10.1007/3-540-48234-2_11]
[113] Regan P, Hamilton S. NASA’s mission reliable. Computer, 2004, 37(1): 59–68. [doi: 10.1109/MC.2004.1260727]
[114] Lamport L. The PlusCal algorithm language. In: Proc. of the 6th Int’l Colloquium on Theoretical Aspects of Computing. Malaysia:
Springer, 2009. 36–60. [doi: 10.1007/978-3-642-03466-4_2]
[115] Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. P: Safe asynchronous event-driven programming. In: Proc. of the 34th
ACM SIGPLAN Conf. on Programming Language Design and Implementation. Seattle: ACM, 2013. 321–332. [doi: 10.1145/2491956.
2462184]
[116] Shapiro M, Preguiça N, Baquero C, Zawirski M. Conflict-free replicated data types. In: Proc. of the 13th Int’l Symp. on Stabilization,
Safety, and Security of Distributed Systems. Grenoble: Springer, 2011. 386–400. [doi: 10.1007/978-3-642-24550-3_29]
[117] Zave P. Using lightweight modeling to understand chord. ACM SIGCOMM Computer Communication Review, 2012, 42(2): 49–57.
[doi: 10.1145/2185376.2185383]
[118] Ongaro D. Consensus: Bridging Theory and Practice. Stanford: Stanford University, 2014.
[119] Gu XS, Wei HF, Qiao L, Huang Y. Raft with out-of-order executions. Ruan Jian Xue Bao/Journal of Software, 2021, 32(6): 1748–1778
(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6248.htm [doi: 10.13328/j.cnki.jos.006248]
[120] Yi XC, Wei HF, Huang Y, Qiao L, Lü J. TPaxos consensus protocol in PaxosStore: Derivation, specification, and refinement. Ruan Jian
Xue Bao/Journal of Software, 2020, 31(8): 2336–2361 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5964.htm
[doi: 10.13328/j.cnki.jos.005964]
[121] Vanlightly J. TLA+ specifications for Kafka. 2023. https://github.com/Vanlightly/kafka-tlaplus
[122] Howard H, Kuppe MA, Ashton E, Chamayou A, Crooks N. Smart casual verification of the confidential consortium framework. In:
Proc. of the 22nd USENIX Symp. on Networked Systems Design and Implementation. Philadelphia: USENIX Association, 2025. 15.
[123] TLA+ specifications and trace validation for etcd. 2024.https://github.com/etcd-io/raft/tree/main/tla
+
[124] Ouyang LZ, Huang Y, Huang BY, Ma XX. Leveraging TLA specifications to improve the reliability of the ZooKeeper coordination