Dynamic Partial-Order Reduction for Model Checking Software

We present a new approach to partial-order reduction for model checking software. This approach is based on dynamically tracking interactions between concurrent processes/threads during model checking, and then exploiting this information using a new partial-order reduction algorithm to identify backtracking points where alternative paths in the state space need to be explored. We present examples of multi-threaded programs where our dynamic partial-order reduction technique can significantly reduce the search space while traditional partial-order algorithms are helpless.