This paper discusses a generalised incremental hashing scheme for explicit state model checkers. The hashing scheme has been implemented into the model checker Spin. The incremental hashing scheme works for Spin’s exhaustive and both approximate verification modes: bitstate hashing and hash compaction. An implementation is provided for 32-bit and 64-bit architectures.
We performed extensive experiments on the BEEM benchmarks to compare the incremental hash functions against Spin’s traditional hash functions. In almost all cases, incremental hashing is faster than traditional hashing. The amount of performance gain depends on several factors, though.
We conclude that incremental hashing performs best for the (64-bits) Spin’s bitstate hashing mode, on models with large state vectors, and using a verifier, that is optimised by the C compiler.
|Title of host publication||Model Checking Software|
|Subtitle of host publication||15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings|
|Editors||K. Havelund, R. Majumdar, J. Palsberg|
|Place of Publication||Berlin, Heidelberg|
|Number of pages||18|
|Publication status||Published - Aug 2008|
|Event||15th International SPIN Workshop on Model Checking Software 2008 - Los Angeles, United States|
Duration: 10 Aug 2008 → 12 Aug 2008
Conference number: 15
|Name||Lecture Notes in Computer Science|
|Name||Theoretical Computer Science and General Issues|
|Workshop||15th International SPIN Workshop on Model Checking Software 2008|
|Period||10/08/08 → 12/08/08|
- FMT-MC: MODEL CHECKING
- n/a OA procedure