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.
http://hdl.handle.net/11583/2573937
Titolo: | To split or to group: from divide-and-conquer to sub-task sharing in verifying multiple properties |
Autori: | |
Data di pubblicazione: | 2014 |
Abstract: | 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. |
Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
wor14-01.pdf | 2. Post-print | Non Pubblico - Accesso privato/ristretto | Administrator Richiedi una copia |