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.

People

Publications

2013

2011

2009

‚Äč