  In this paper we introduce a novel way to speed up the discovery of
counterexamples in bounded model checking, based on parallel runs over versions
of a system in which features have been randomly disabled. As shown in previous
work, adding constraints to a bounded model checking problem can reduce the
size of the verification problem and dramatically decrease the time required to
find counterexample. Adapting a technique developed in software testing to this
problem provides a simple way to produce useful partial verification problems,
with a resulting decrease in average time until a counterexample is produced.
If no counterexample is found, partial verification results can also be useful
in practice.
