Coverage of Implementations by Simulating Specifications
========================================================

In formal verification, we verify that an implementation is correct with
respect to a specification. When verification succeeds and the implementation
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 implementation. In this paper we study coverage for simulation-based
formal verification, where both the implementation and the
specification are modelled by labeled state-transition graphs,
and an implementation $\I$ satisfies a specification $\S$ if $\S$
simulates $\I$. Our measure of coverage is based 
on small modifications we apply to $\I$. A part of $\I$ is 
covered by $\S$ if the mutant implementation in which this part is
modified is no longer simulated by $\S$. Thus, ``mutation coverage''
tells us which parts of the implementation were actually essential
for the success of the verification. We describe two algorithms
for finding the parts of the implementation that are covered by $\S$.
The first algorithm improves a naive algorithm that checks the mutant
implementations one by one by exploiting the significant overlaps among
the mutant implementations. The second algorithm is symbolic, and it
improves a naive symbolic algorithm by reducing the number of 
variables in the OBDDs involved. In addition, we compare our
coverage measure with other approaches for measuring coverage.