  This publication introduces A State Space Exploration Tool that is based on
representing the model under verification as a piece of C++ code that obeys
certain conventions. Its name is ASSET. Model checking takes place by compiling
the model and the tool together, and executing the result. This approach
facilitates very fast execution of the transitions of the model. On the other
hand, the use of stubborn sets and symmetries requires that either the modeller
or a preprocessor tool analyses the model at a syntactic level and expresses
stubborn set obligation rules and the symmetry mapping as suitable C++
functions. The tool supports the detection of illegal deadlocks, safety errors,
and may progress errors. It also partially supports the detection of must
progress errors.
