Fast, All-Purpose State Storage

Existing techniques for approximate storage of visited states in a model checker are too special-purpose and too DRAM-intensive. Bitstate hashing, based on Bloom filters, is good for exploring most of very large state spaces, and hash compaction is good for high-assurance verification of more tractable problems. We describe a scheme that is good at both, because it adapts at run time to the number of states visited. It does this within a fixed memory space and with remarkable speed and accuracy. In many cases, it is faster than existing techniques, because it only ever requires one random access to main memory per operation; existing techniques require several to have good accuracy. Adapting to accomodate more states happens in place using streaming access to memory; traditional rehashing would require extra space, random memory accesses, and hash computation. The structure can also incorporate search stack matching for partial-order reductions, saving the need for extra resources d...

• Type: Conference
• Year: 2009
• Where: SPIN
• Authors: Peter C. Dillinger, Panagiotis Manolios
• Keywords: Large State Spaces, Random Memory Accesses, SPIN 2009, Theoretical Computer Science, fixed Memory Space