Stateful dynamic partial-order reduction

State space explosion is the main obstacle for model checking concurrent programs. Among the solutions, partial-order reduction (POR), especially dynamic partial-order reduction (DPOR) [1], is one of the promising approaches. However, DPOR only supports stateless explorations for acyclic state spaces. In this paper, we present the stateful DPOR approach for may-cyclic state spaces, which naturally combines DPOR with stateful model checking to achieve more efficient reduction. Its basic idea is to summarize the interleaving information for all transition sequences starting from each visited state, and infer the necessary partial-order information based on the summarization when a visited state is encountered again. Experiment results on two programs coming from [1] show that both of the costs of space and time could be remarkably reduced by stateful DPOR with rather reasonable extra memory overhead. © Springer-Verlag Berlin Heidelberg 2006.