Sciweavers

Share
DAC
2010
ACM

Coverage in interpolation-based model checking

9 years 6 months ago
Coverage in interpolation-based model checking
Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art SATbased Model Checking using Craig interpolation. The key insight of our algorithm is to re-use previously computed inductive invariants and counterexamples. This re-use permits a quick conclusion of the vast majority of tests, and enables the computation of a coverage measure with 96% accuracy with only 5x the runtime of the Model Checker. Categories and Subject Descriptors B.6.3 [Logic Design]: Design aids—Verification General Terms Verification, Algorithms
Hana Chockler, Daniel Kroening, Mitra Purandare
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where DAC
Authors Hana Chockler, Daniel Kroening, Mitra Purandare
Comments (0)
books