Combining Partial Order Reduction with Bounded Model Checking

Model checking is an efficient technique for verifying properties on reactive systems. Partial-order reduction (POR) and symbolic model checking are two com- mon approaches to deal with the state space explosion problem in model checking. Traditionally, symbolic model checking uses BDDs which can suffer from space blow- up. More recently bounded model checking (BMC) using SAT-based procedures has been used as a very successful alternative to BDDs. However, this approach gives poor results when it is applied to models with a lot of asynchronism. This paper presents an algorithm which combines partial order reduction methods and bounded model check- ing techniques in an original way that allows efficient verification of temporal logic properties (LT LX ) on models featuring asynchronous processes. The encoding to a SAT problem strongly reduces the complexity and non-determinism of each transition step, allowing efficient analysis even with longer execution traces. The starting-point of our work is the Two-Phase algorithm (Namalesu and Gopalakrishnan) which per- forms partial-order reduction on process-based models. At first, we adapt this algo- rithm to the bounded model checking method. Then, we describe our approach for- mally and demonstrate its validity. Finally, we present a prototypal implementation and report encouraging experimental results on a small example