Formal Verification of a Partial-Order Reduction Technique for Model-Checking

Mechanical theorem proving and model checking are the two main methods of formal verification, each with its own strengths and weaknesses. Mechanical theorem proving is completely general, but requires intensive human guidance. Model checking is automatic, but is applicable to only certain types of problems. Clearly, these two methods should be combined so that their strengths and weaknesses complement each other. Prior research in this direction has focused on how to decompose a verification problem into parts each of which is manageable by one of the two methods. In this paper, we explore another possibility: we use mechanical theorem proving to formally verify the metatheory of model checking. As a case study, we use the mechanical theorem prover HOL to verify the correctness of a partial-order reduction technique for cutting down the amount of state search performed by model checkers.