Exploring Clause Symmetry in a Distributed Bounded Model Checking Algorithm

In recent years new and efficient symbolic model checking algorithms have been developed. One technique, bounded model checking or BMC, has been particularly promising. BMC models the system being verified as a boolean formula whose satisfying assignments provide counterexamples for properties verified. BMC unrolls the system in its multiple iterations. Because of this the structure of the formula representing the system is very symmetric, since all iterations are similar in structure. This work explores this symmetry in a distributed algorithm by postponing the unrolling of the formulas until they are used. This minimizes communication among processors since the formulas transmitted are shorter. Moreover, avoiding the unrolling of conflict clauses has a more pronounced effect, because due to the symmetric nature of the formula, a conflict clause for one instant in the execution can be applied to multiple time instants. As a consequence, short conflict clauses can be unrolled into much more effective clauses, cutting back on the search space significantly. In our experiments we have obtained gains of up to three orders of magnitude in verification time and up to two orders of magnitude in memory usage in large examples