To Split or to Group: From Divide-and-Conquer to Sub-Task Sharing for Verifying Multiple Properties in Model Checking

Hardware systems complexity has constantly increased in recent years. Guaranteeing their correctness is a must. Formal verification techniques, like model checking, now play a major role in industrial environments. Their efficiency in dealing with large sets of properties is crucial. This paper deals with property grouping, decomposition, and coverage in model checking. Property grouping is a valuable solution whenever several properties must be proven for a single model. As such sets may include "easy-to-prove" and/or "similar" properties, grouping can reduce overhead avoiding sub-tasks repetition. Property decomposition, following the divide-and-conquer paradigm, can be effective whenever a property turns out to be "hard-to-prove". Our contribution is a heuristic property manager, running on top of a multi-engine model checking portfolio, aiming at productivity optimization. We compare different clustering heuristics and we exploit decomposition strategies for property sub-setting. We also consider the problem of evaluating a coverage measure for properties, used to monitor the "advancement" of the verification task.