Sciweavers

Share
POPL
2005
ACM

Dynamic partial-order reduction for model checking software

11 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)
books