Decades of research has resulted in dozens of automatic verification
engines including SPIN~\cite{holzmann03}, NuSMV~\cite{cimatti00},
Salsa~\cite{bharadwaj00}, and our own Lurch~\cite{owen03a}.  A
standard paper in the field might offer guidance on what tool to
use in particular circumstances.  For example, Cobleigh
et.al.~\cite{cobleigh01} recommend using different  verification
engines at different points of the software lifecycle.  Also
Smith~\cite{smith04} argues that NuSMV/SPIN are best suited to the
verification of hardware/software specifications (respectively).

@misc{smith04,
	title="Model Checking of Artificial Intelligence Based Planners, annual report",
	author="Margaret Smith",
	year=2005,
	notes="Download from \url{http://sarpresults.ivv.nasa.gov/ViewResearch/57.jsp}"
}

This paper argues {\em against} using these tools in isolation.
We show here that 
these engines offer {\em complementary} results;
i.e.  a defect that is easy to recognize on one engine may be
difficult or impossible to  find using another.  Hence, by {\em
combining} these tools, we may learn more than than just using them
in isolation. Further, we can learn those lessons faster.
In the experiments shown below, we sort our specification engines
on their expected runtime. We run the slower tools only if the faster tools
fail to find defects. As shown in our experiments, this
{\em cascaded} approach can find defects much
sooner that an {\em isolated} approach.

Another benefit of using combination of tools
is the discovery of defects in the tools themselves. 
A {\em verification system} is a combination of a verification engine (e.g. SPIN,
NuSMV, SALSA, Lurch) {\em plus} the tools used to {\em translate} some
specification into the internal format required for that engine.
This pair of \[verification\;system=\{engine,\; translator\}\] 
can be an intricate piece of software
with, potentially, many quirks:
\bi
\item  
If multiple tools,
representing diverse modeling languages, translation assumptions,
and verification engines, can be run on the same input to produce
consistent results, the user can be much more confident in the
results' correctness.
\item
Also, by comparing the output of multiple systems, it is possible to find and fix
bugs in (say) the translators. For example, where the use of combinations of
verification systems lead to the discovery of previously undetected
errors in our
translators.
\ei
The ability of combinations of verification systems to uncover
translator errors is a particular advantage of this approach.
Having written  and used several such translators, we are now uncomfortable
when a researcher asserts ``my translator has no errors''.  How can
they be so sure? 
Translation  can be a non-trivial task.
For example, depending on the decisions made during translation,
there can be orders of magnitude difference in the performance of the
verification engine between two
two different translations from one language to
the same verification engine~\cite{norvig03}. 
One way to increase
our level of certification in a translator is to increase our experience-base
with that translator.
Using combinations of verification systems is one way to increase
the experience base of all parts of a verification system, including
the translators. 

@book{norvig03,
 author = {Stuart J. Russell and Peter Norvig and John F. Candy and Jitendra M. Malik and Douglas D. Edwards},
 title = {Artificial intelligence: a modern approach},
 year = {2003},
 pages = {97-104},
 isbn = {0-13-103805-2},
 publisher = {Prentice-Hall, Inc.},
 address = {Upper Saddle River, NJ, USA},
 }

One drawback with  our proposal is that users have a hard enough
time running one translation system, let alone multiple versions.
Having said that, our work highlights the advantages of combining
verification systems. A future direction that arises from our work
is simplifying the overhead associated of moving specifications and
properties between verification systems. There are early signs that
the research community is moving in that direction. For example,
the BEEM website\footnote{Benchmarks for Explicit Model checkers  
\url{http://anna.fi.muni.cz/models/}.} lists an extensive
benchmark suite for explicitly model checkers.    To use the
benchmarks, researchers must build a translator from the syntax
used at this site into their own local format. Given a back-translator
(from the local format back to the BEEM format), then the  BEEM syntax
could become a {\em lingua franca} connecting together multiple verification
systems and enabling our proposal to use multiple verification systems.

