🚀 go-pugleaf

             ����|��T��  ���զw�դh


             SGM: A User-Friendly Verification Environment

                              Abstract

Model-checking often faces the problem of reducing 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 verification tools do not
completely allow a user 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". Without being a verification expert, a user can still use
the graphical interface of SGM to manipulate state-graphs for better
verification efficiency. Thus, SGM tries to bridge the gap between
profound verification theory and practical use of verification.
Further, we are also proposing three new state-space reduction techniques,
namely Read-Write Analysis, Bypass Internal Transitions, and
Sibling Transition Multiplicity Reduction. They are implemented into
SGM and experiments have been conducted to show their usefulness.