Refining dependencies improves partial-order verification methods

Abstract

Partial-order verification methods exploit “independency” between transitions of a concurrent program to avoid parts of the state space explosion due to the modeling of concurrency by interleaving. In this paper, we study the influence of refining dependencies between transitions of the program on the effectiveness of these methods. We show that carefully tracking dependencies can yield substantial improvements for their performances. For instance, we were able to decrease the memory requirements needed for the verification of a real-size protocol with such a method from a factor of 5 to a factor of 25 by only refining dependencies.