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 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. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Algorithms, Verification, Reliability Keywords Partial-order reduction, software model checking

• Type: Conference
• Year: 2005
• Where: POPL
• Authors: Cormac Flanagan, Patrice Godefroid
• Keywords: General Terms Algorithms, Partial-order Reduction, POPL 2005, Programming Languages, Various Concurrent Processes/threads