| |
|
|
Coverage Estimation for Symbolic Model Checking
AbstractThis talk presents a coverage metric for model checking based verification. Although model checking is exhaustive with respect to the verified properties, a bug can still escape detection if the erroneous behavior caused by the bug does not violate any verified property. The coverage metric proposed here estimates the "completeness" of a set of properties. A symbolic algorithm to compute this metric for a subset of CTL will also be presented that is of the same order of complexity as a model checking algorithm. Experimental results on several test cases show that this metric has value in increasing confidence in the correctness of the circuit. |