The current technology of verification engineering requires well-trained
personnels in logics and automaton theory, who carefully tune their
verification packages, to tame the well-known state-space explosion
problem.
Several researches have resulted in a large number of techniques
for reducing the system state-space, such as symmetry-based reductions,
partial-order semantics, bisimulation equivalences, etc.
To let more people benefit from the technology of
computer-aided verification even with little training in the related
theories, a new tool called State-Graph Manipulator (SGM) was
developed to package various sophisticated verification techniques
as manipulators on state-graphs as high-level data-objects.
An example user session of SGM is
discussed and the results presented.
Experiments conducted using SGM show how the tool, when used by a system
designer, can increase verification efficiency and scalability.