To split or to group: from divide-and-conquer to sub-task sharing in verifying multiple properties

This paper addresses the issue of property grouping, property decomposition, and property coverage in model checking problems. Property grouping, i.e., clustering, is a valuable solution whenever (very) large sets of properties have to be proven for a given model. As such sets often include many “easy-to-prove” and/or “similar” properties, property grouping can reduce overheads, and avoid reiteration on common sub-tasks. On the other end of the spectrum, property decomposition can be effective whenever a given property turns-out (or it is expected) to be “hard-to-prove”. Decomposition of properties into “sub-properties” follows the divide-and-conquer paradigm, and it shares with this paradigm advantages and disadvantages. Our contribution is to present a heuristic property manager, running on top of a multi-engine model checking portfolio, with the specific target of optimizing productivity. We discuss, and compare, different clustering heuristics, and we exploit circuit de-composition strategies for property sub-setting. We also consider the problem of evaluating a coverage measure for properties, where the “coverage” is used to monitor the “advancement” during the (partial) verification of a given property. We finally consider estimates of the bound of a property as a measure of confidence in BMC runs. We include preliminary experimental data indicating that the proposed approaches can provide improvements over state-of-the-art methods potentially enhancing productivity in industrial environments.