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

2198 软件学报 2026 年第 37 卷第 5 期

[74] Visser W, Havelund K, Brat GP, Park S. Model checking programs. In: Proc. of the 15th IEEE Int’l Conf. on Automated Software
Engineering. Grenoble: IEEE, 2000. 3–12. [doi: 10.1109/ASE.2000.873645]
[75] Bokor P, Kinder J, Serafini M, Suri N. Supporting domain-specific state space reductions through local partial-order reduction. In: Proc.
of the 26th IEEE/ACM Int’l Conf. on Automated Software Engineering. Lawrence: IEEE, 2011. 113–122. [doi: 10.1109/ASE.2011.
6100044]
[76] Rodriguez A, Killian C, Bhat S, Kostić D, Vahdat A. Macedon: Methodology for automatically creating, evaluating, and designing
overlay networks. In: Proc. of the 1st Conf. on Symp. on Networked Systems Design and Implementation. San Francisco: USENIX
Association, 2004. 20.
[77] Godefroid P. Model checking for programming languages using VeriSoft. In: Proc. of the 24th ACM SIGPLAN-SIGACT Symp. on
Principles of Programming Languages. Paris: ACM, 1997. 174–186. [doi: 10.1145/263699.263717]
[78] Liu XZ, Lin W, Pan AM, Zhang Z. WiDS checker: Combating bugs in distributed systems. In: Proc. of the 4th USENIX Conf. on
Networked Systems Design & Implementation. Cambridge: USENIX Association, 2007. 19.
[79] Geels D, Altekar G, Maniatis P, Roscoe T, Stoica I. Friday: Global comprehension for distributed replay. In: Proc. of the 4th USENIX
Conf. on Networked Systems Design & Implementation. Cambridge: USENIX Association, 2007. 21.
[80] Yuan XH, Yang JF. Effective concurrency testing for distributed systems. In: Proc. of the 25th Int’l Conf. on Architectural Support for
Programming Languages and Operating Systems. Lausanne: ACM, 2020. 1141–1156. [doi: 10.1145/3373376.3378484]
[81] Scott C, Panda A, Brajkovic V, Necula G, Krishnamurthy A, Shenker S. Minimizing faulty executions of distributed systems. In: Proc.
of the 13th USENIX Conf. on Networked Systems Design and Implementation. Santa Clara: USENIX Association, 2016. 291–309.
[82] Wang D, Dou WS, Gao Y, Wu CN, Wei J, Huang T. Model checking guided testing for distributed systems. In: Proc. of the 18th
European Conf. on Computer Systems. Rome: ACM, 2023. 127–143. [doi: 10.1145/3552326.3587442]
[83] Geels D, Altekar G, Shenker S, Stoica I. Replay debugging for distributed applications. In: Proc. of the 2006 USENIX Annual Technical
Conf. Boston: USENIX Association, 2006. 27.
[84] Zhou JY, Xu M, Shraer A, Namasivayam B, Miller A, Tschannen E, Atherton S, Beamon AJ, Sears R, Leach J, Rosenthal D, Dong X,
Wilson W, Collins B, Scherer D, Grieser A, Liu Y, Moore A, Muppana B, Su XG, Yadav V. FoundationDB: A distributed unbundled
transactional key value store. In: Proc. of the 2021 Int’l Conf. on Management of Data. ACM, 2021. 2653–2666. [doi: 10.1145/3448016.
3457559]
[85] Antithesis: Autonomous software testing. 2018. https://antithesis.com/
[86] Sled simulation guide (jepsen-proof engineering). 2020. http://sled.rs/simulation.html
[87] MadSim: Magical deterministic simulator for distributed systems in Rust. 2021. https://github.com/madsim-rs/madsim
[88] tokio-rs/turmoil. Tokio. 2022. https://github.com/tokio-rs/turmoil
3
[89] Liu XZ, Guo ZY, Wang X, Chen FB, Lian XC, Tang J, Wu M, Kaashoek MF, Zhang Z. D S: Debugging deployed distributed systems.
In: Proc. of the 5th USENIX Symp. on Networked Systems Design and Implementation. San Francisco: USENIX Association, 2008.
423–437.
[90] Pshenichkin A. So you think you want to write a deterministic hypervisor? 2024. https://antithesis.com/blog/deterministic_hypervisor/
[91] Clarke EM Jr, Grumberg O, Peled DA. Model Checking. Cambridge: MIT Press, 1999.
[92] Godefroid P. Partial-order Methods for the Verification of Concurrent Systems. Berlin, Heidelberg: Springer, 1996. [doi: 10.1007/3-540-
60761-7]
[93] Godefroid P. Using partial orders to improve automatic verification methods. In: Proc. of the 2nd Int’l Conf. on Computer-aided
Verification. New Brunswick: Springer, 1991. 176–185. [doi: 10.1007/BFb0023731]
[94] Mazurkiewicz A. Trace theory. In: Brauer W, Reisig W, Rozenberg G, eds. Petri Nets: Applications and Relationships to Other Models
of Concurrency. Berlin, Heidelberg: Springer, 1987. 278–324. [doi: 10.1007/3-540-17906-2_30]
[95] Livshits B, Sridharan M, Smaragdakis Y, Lhoták O, Amaral JN, Chang BYE, Guyer SZ, Khedker UP, Møller A, Vardoulakis D. In
defense of soundiness: A manifesto. Communications of the ACM, 2015, 58(2): 44–46. [doi: 10.1145/2644805]
[96] Emerson EA, Sistla AP. Symmetry and model checking. In: Proc. of the 5th Int’l Conf. on Computer Aided Verification. Elounda:
Springer, 1993. 463–478. [doi: 10.1007/3-540-56922-7_38]
[97] Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. In: Proc. of the 32nd ACM SIGPLAN-SIGACT
Symp. on Principles of Programming Languages. Long Beach: ACM, 2005. 110–121. [doi: 10.1145/1040305.1040315]
[98] Yang Y, Chen XF, Gopalakrishnan G, Kirby RM. Efficient stateful dynamic partial order reduction. In: Proc. of the 15th Int’l Workshop
on Model Checking Software. Los Angeles: Springer, 2008. 288–305. [doi: 10.1007/978-3-540-85114-1_20]
[99] Trimananda R, Luo WY, Demsky B, Xu GH. Stateful dynamic partial order reduction for model checking event-driven applications that