Dos and don'ts of CTL state coverage estimation

Coverage estimation for model checking quantifies the completeness of a set of properties. We present an improved version of the algorithm of Hoskote et al. [7] that applies to a larger subset of CTL; we prove properties of the algorithm and apply it to three case studies. From these case studies we derive recommendations for an effective use of coverage estimation. Categories and Subject Descriptors B.6.3 [Logic design]: Design aids—Verification General Terms: Verification, Algorithms

• Type: Conference
• Year: 2003
• Where: DAC
• Authors: Nikhil Jayakumar, Mitra Purandare, Fabio Somenzi
• Keywords: Aids—verification General Terms, Case Studies, Computer Architecture, Coverage Estimation, DAC 2003