MODIST is a practical software model checker for unmodified concurrent, distributed and cloud systems. MODIST explores different execution paths systematically as well as simulating a variety of environment faults to discover subtle corner-case defects. We have applied MODIST in Oracle Berkely DB, MPS(Paxos implementation), SQL Azure, Windows Azure Storage and other real systems, and found many new bugs.
- Haoxiang Lin, Model Checking Distributed Systems (in Chinese), in Communications of The CCF, vol. 9, no. 2, pp. 46-51, China Computer Federation, February 2013.
- Huayang Guo, Ming Wu, Lidong Zhou, Gang Hu, Junfeng Yang, and Lintao Zhang, Practical software model checking via dynamic interface reduction, Symposium on Operating Systems Principles (SOSP), October 2011.
- Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou, MODIST: Transparent Model Checking of Unmodified Distributed Systems, in Proceedings of the 6th Symposium on Networked Systems Design and Implementation (NSDI '09), USENIX, 22 April 2009.