Enhanced Probabilistic Verification with 3Spin and 3Murphi
Peter C. Dillinger and Panagiotis Manolios.
SPIN 2005, 12th International SPIN Workshop on Model Checking of Software. © Springer-Verlag
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