|
PLDog submit an article | search | rss feed | register | feedback | about |
| Dynamic Partial Order Reduction of Model Checking Software | |||
|
|||
| 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 | |||
|
|||