Dynamic partial-order reduction for model checking software

12 years 1 months ago
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
Cormac Flanagan, Patrice Godefroid
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where POPL
Authors Cormac Flanagan, Patrice Godefroid
Comments (0)