home · mobile · calendar · colloquia · 2001-2002 · 

Colloquium - Kupferman

Coverage Metrics for Model Checking
Hebrew University, Israel

In formal verification, we verify that a system is correct with respect to a specification. When verification succeeds and the system is proven to be correct, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. Coverage metrics are based on modifications we apply to the system in order to check which parts of it were actually relevant for the verification process to succeed. Coverage metrics are successfully used in simulation-based verification. In the talk, I will discuss coverage metrics for model checking. I will describe some principle that we believe should be part of any coverage metric for model checking, suggest several coverage metrics that apply these principles, and describe algorithms for finding the uncovered parts of a system under these definitions.

Joint work with Hana Chockler, Robert Kurshan, and Moshe Vardi.
Hosted by Fabio Somenzi, Department of Electrical and Computer Engineering.
Refreshments will be served in ECOT 832 following the talk.

Department of Computer Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
May 5, 2012 (14:13)