User-friendly verification

Model checking often faces the problem of reducing the large exponential sizes of state-space representations. Several reduction techniques such as bisimulation equivalence, partial-order semantics, and symmetry-based reduction have been proposed, but existing tools do not completely allow a user the flexibility in manipulating state spaces. We propose a new user-friendly verification environment where a user has full control on what techniques to apply and in what sequences to apply them. We have implemented the environment in a tool called State-Graph Manipulators (SGM). SGM packages verification techniques into efficient, reusable, modular manipulators, that act on high-level state-space representations called state-graphs. Further, we are also proposing four new state space reduction techniques, namely variable shielding, read-write analysis, internal transitions bypassing, and sibling transition multiplicity reduction. They are implemented into SGM and experiments have been conducted to show their usefulness.