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

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

SIGPLAN Int’l Conf. on Functional Programming. Freiburg: ACM, 2007. 125–136. [doi: 10.1145/1291151.1291171]
[48] Musuvathi M, Qadeer S, Ball T, Basler G, Nainar PA, Neamtiu I. Finding and reproducing Heisenbugs in concurrent programs. In: Proc.
of the 8th USENIX Conf. on Operating Systems Design and Implementation. San Diego: USENIX Association, 2008. 267–280.
[49] Yang JF, Chen ST, Wu M, Xu ZL, Liu XZ, Lin HX, Yang M, Long F, Zhang LT, Zhou LD. MoDist: Transparent model checking of
unmodified distributed systems. In: Proc. of the 6th USENIX Symp. on Networked Systems Design and Implementation. Boston:
USENIX Association, 2009. 213–228.
[50] Yabandeh M, Knezevic N, Kostic D, Kuncak V. CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems.
In: Proc. of the 6th USENIX Symp. on Networked Systems Design and Implementation. Boston: USENIX Association, 2009. 229–244.
[51] Basset: A tool for systematic testing of actor programs. 2009. https://mir.cs.illinois.edu/basset/
[52] Lauterburg S, Dotta M, Marinov D, Agha G. A framework for state-space exploration of Java-based actor programs. In: Proc. of the
2009 IEEE/ACM Int’l Conf. on Automated Software Engineering. Auckland: IEEE, 2009. 468–479. [doi: 10.1109/ASE.2009.88]
[53] ISP. 2009. https://github.com/cogumbreiro/isp
[54] Vo A, Vakkalanka S, DeLisi M, Gopalakrishnan G, Kirby RM, Thakur R. Formal verification of practical MPI programs. In: Proc. of
the 14th ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming. Raleigh: ACM, 2009. 261–270. [doi: 10.1145/
1504176.1504214]
[55] Simsa J, Bryant R, Gibson G. dBug: Systematic testing of distributed and multi-threaded systems (software repository). 2010. https://
www.cs.cmu.edu/~jsimsa/dbug/
[56] Simsa J, Bryant R, Gibson G. dBug: Systematic evaluation of distributed systems. In: Proc. of the 5th Int’l Workshop on Systems
Software Verification. Voncouver: USENIX Association, 2010. 3.
[57] Guerraoui R, Yabandeh M. Model checking a networked system without the network. In: Proc. of the 8th USENIX Conf. on Networked
Systems Design and Implementation. Boston: USENIX Association, 2011. 225–238.
[58] MP-Basset. 2011. https://ssg.lancs.ac.uk/research/tools/mp-basset/
[59] Bokor P, Kinder J, Serafini M, Suri N. Efficient model checking of fault-tolerant distributed protocols. In: Proc. of the 41st IEEE/IFIP
Int’l Conf. on Dependable Systems & Networks. Hong Kong: IEEE, 2011. 73–84. [doi: 10.1109/DSN.2011.5958208]
[60] Saissi H, Bokor P, Muftuoglu CA, Suri N, Serafini M. Efficient verification of distributed protocols using stateful model checking. In:
Proc. of the 32nd Int’l Symp. on Reliable Distributed Systems. Braga: IEEE, 2013. 133–142. [doi: 10.1109/SRDS.2013.22]
[61] Artho C, Hagiya M, Potter R, Tanabe Y, Weitl F, Yamamoto M. Software model checking for distributed systems with selector-based,
non-blocking communication. In: Proc. of the 28th IEEE/ACM Int’l Conf. on Automated Software Engineering. Silicon Valley: IEEE,
2013. 169–179. [doi: 10.1109/ASE.2013.6693077]
[62] Leungwattanakit W, Artho C, Hagiya M, Tanabe Y, Yamamoto M, Takahashi K. Modular software model checking for distributed
systems. IEEE Trans. on Software Engineering, 2014, 40(5): 483–501. [doi: 10.1109/TSE.2013.49]
[63] Concuerror. 2013. https://concuerror.com/
[64] Christakis M, Gotovos A, Sagonas K. Systematic testing for detecting concurrency errors in Erlang programs. In: Proc. of the 6th IEEE
Int’l Conf. on Software Testing, Verification and Validation. Luxembourg: IEEE, 2013. 154–163. [doi: 10.1109/ICST.2013.50]
[65] SAMC. 2014. https://ucare.cs.uchicago.edu/projects/samc/
[66] FlyMC. 2019. https://ucare.cs.uchicago.edu/projects/FlyMC/
[67] Lukman JF, Ke H, Stuardo CA, Suminto RO, Kurniawan DH, Simon D, Priambada S, Tian C, Ye F, Leesatapornwongsa T, Gupta A, Lu
S, Gunawi HS. FlyMC: Highly scalable testing of complex interleavings in distributed systems. In: Proc. of the 14th EuroSys Conf.
Dresden: ACM, 2019. 20. [doi: 10.1145/3302424.3303986]
[68] DSLabs. 2019. https://github.com/emichael/dslabs
[69] Michael E, Woos D, Anderson T, Ernst MD, Tatlock Z. Teaching rigorous distributed systems with efficient model checking. In: Proc.
of the 14th EuroSys Conf. 2019. Dresden: ACM, 2019. 32. [doi: 10.1145/3302424.3303947]
[70] SandTable. 2024. https://github.com/tangruize/SandTable
[71] Tang RZ, Sun XD, Huang Y, Wei YY, Ouyang LZ, Ma XX. SandTable: Scalable distributed system model checking with specification-
level state exploration. In: Proc. of the 19th European Conf. on Computer Systems. Athens: ACM, 2024. 736–753. [doi: 10.1145/
3627703.3650077]
[72] Remix. 2025. https://github.com/Lingzhi-Ouyang/Remix
[73] Ouyang LZ, Sun XD, Tang RZ, Huang Y, Jivrajani M, Ma XX, Xu TY. Multi-grained specifications for distributed system model
checking and verification. In: Proc. of the 20th European Conf. on Computer Systems. Rotterdam: ACM, 2025. 379–395. [doi: 10.1145/
3689031.3696069]