8/3/2001
4:00pm-5:00pm
ECOT 831
|
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.
|
The Department holds colloquia throughout the Fall and Spring semesters. These
colloquia, open to the public, are typically held on Thursday afternoons, but
sometimes occur at other times as well.
If you would like to receive email notification of upcoming colloquia,
subscribe to our
Colloquia Mailing List.
If you would like to schedule a colloquium, see
Colloquium Scheduling.
Sign language interpreters are available upon request. Please contact
Stephanie Morris at least five days prior to the colloquium.
|
