Combining partial order reductions with on-the-fly model-checking

Abstract

Partial order model-checking is an approach to reduce time and memory in model-checking concurrent programs. On-the-fly model-checking is a technique to eliminate part of the search by intersecting the (negation of the) checked property with the state space during its generation. We prove conditions under which these two methods can be combined in order to gain from both reductions. An extension of the model-checker SPIN, which implements this combination, is studied, showing substantial reduction over traditional search, not only in the number of reachable states, but directly in the amount of memory and time used.