The symbolic model checker in STeP is specialized to checking linear
time temporal properties of fair transition systems. For invariants
it performs a specialized backwards search using, if possible,
auxiliary invariants to prune the search space. This means that invariants
that are inductive relative to previously established (or generated invariants)
are checked in a single iteration of the model checker.
The performance of this approach depends critically on the supply of
auxiliary invariants as our example will show.
