| Dynamic Partial Order Reduction of Model Checking Software |
| Posted by: Ray |
5:35pm, Saturday, 24 November 2007 |
|
| We present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored. We present examples of multi-threaded programs where our new dynamic partial-order reduction technique significantly reduces the search space, even though traditional partial-order algorithms are helpless. |
| Cormac Flanagan and Patrice Godefroid |
| Appears in POPL 2005 |
|
|