Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction

We propose a new method for reducing the interleaving space dur-ing stateless model checking of multithreaded C/C++ programs. The problem is challenging because of the exponential growth of possible interleavings between threads. We have developed a new method, called assertion guided abstraction, which leverages both static and dynamic program analyses in a cooperative framework to reduce the interleaving space. Unlike existing methods that con-sider all interleavings of all conflicting memory accesses in a pro-gram, our new method relies on a new notion of predicate depen-dence based on which we can soundly abstract the interleaving space to only those conflicting memory accesses that may cause assertion violations and/or deadlocks. Our experimental evaluation of assertion guided abstraction on open source benchmarks shows that it is capable of achieving a significant reduction, thereby al-lowing for the verification of programs that were previously too complex for existing algorithms to handle