manolios@cc.gatech.edu
College of Computing
3Spin and 3Murphi are modified versions of the Spin model checker
and the Murphi verifier. Our modifications enhance the
probabilistic algorithms and data structures for storing visited
states, making them more effective and more usable for verifying
huge transition systems. The tools also support a verification
methodology designed to minimize time to finding errors, or to
reaching desired certainty of error-freedom. This methodology
calls for bitstate hashing, hash compaction, and integrated
analyses of both to provide feedback and advice to the user.
3Spin and 3Murphi are the only tools to offer this support, and
do so with the most powerful and flexible currently-available
implementations of the underlying algorithms and data structures.
PDF (101K) © Springer-Verlag
PS (71K) © Springer-Verlag
|
Last modified: Mon Jun 6 11:29:28 EDT 2005
manolios@cc.gatech.edu |
College of Computing |