Fast, All-Purpose State Storage

13 years 6 months ago
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...
Peter C. Dillinger, Panagiotis Manolios
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SPIN
Authors Peter C. Dillinger, Panagiotis Manolios
Comments (0)