MODIST: Transparent Model Checking of Unmodified Cloud Systems

Established: March 8, 2014

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.