Bojan, 

my new intro killed the following text. it needs to be moved into the end of section 2.B

----------------------------------------

Inspired by West,  we have experimented with a simple random search to
detect errors in software models \cite{owen02a}. Our strategy was as
follows: start at the initial state of the model; choose the next
state at random from those possible; quit when no next state is
possible or a user-specified depth limit is reached. Search results
followed a pattern: at first, many unique states were explored, but
soon the number of unique states explored reached a peak and stopped
increasing; from then on the same states were explored over and
over. When allowed to run to this \textit{saturation} point, at
which the proportion of unique states drops off, the random search
produces surprisingly consistent results.  We concluded that random
search, in spite of its general (worst-case) unreliability, was
sufficiently consistent to pursue as an efficient strategy for
detecting errors in software models
\cite{menzies02,owen02c,owen02b}.

Further work on random search led to the development of Lurch, a
tool for detecting violations of generic and user-defined logical
properties in finite-state machine models \cite{owen03a}. We
compared Lurch's performance to the model checkers SPIN
\cite{holzmann03} and Cadence SMV \cite{mcmillan00} and found that
with random search it is often possible to detect property
violations far more quickly and with orders of magnitude less
memory. We also showed how Lurch could be used together with a
conventional verification tool to greatly improve average
verification performance: use Lurch first for a relatively short
time and only run the verification tool on input models for which
Lurch finds no property violations \cite{owen03b}.

In addition, random search can be used as a \textit{sanity check} on
verification results produced by a model checker:  to improve
performance in real-world applications of model checking, the input
model may be simplified, based on assumptions about its structure.
If the model checker detects no faults in this simplified model,
random search can be run
on an un-simplified version of the model.  Assuming the random
search also detects no faults, we can be more confident in the
simplifying assumptions used to make the input model small enough
for verification with the model checker \cite{owen06}.

 
