Software model checking problems generally contain two different types of non-determinism: 1) non-deterministically chosen values; 2) the choice of interleaving among threads. Most modern software model checkers can handle only one source of non-determinism efficiently, but not both. This paper describes a SAT-based model checker for asynchronous Boolean programs that handles both sources effectively. We address the first type of non-determinism with a form of symbolic execution and fix-point detection. We address the second source of non-determinism using a symbolic and dynamic partial order reduction, which is implemented inside the SAT-solver's case-splitting algorithm. The experimental results show that the new algorithm outperforms the existing software model checkers.
Submitted for publication, a copy is available upon request, 2004, 15 pages.
© 2004 Natasha Sharygina.