Improved probabilistic verification by hash compaction
We present and analyze a probabilistic method for verification by
explicit state enumeration, which improves on the ``hashcompact''
method of Wolper and Leroy. The hashcompact method maintains a hash
table in which compressed values for states instead of full state
descriptors are stored. This method saves space but allows a non-zero
probability of omitting states during verification, which may cause
verification to miss design errors (i.e. verification may produce
``false positives'').
Our method improves on Wolper and Leroy's by calculating the hash and
compressed values independently, and by using a specific hashing
scheme that requires a low number of probes in the hash table. The
result is a large reduction in the probability of omitting a state.
Hence, we can achieve a given upper bound on the probability of
omitting a state using fewer bits per compressed state. For example,
we can reduce the number of bytes stored for each state from the eight
recommended by Wolper and Leroy to only five, and still enumerate
state spaces of up to 80 million reachable states while keeping the
probability of missing even one state to less than 0.13%.
The new verification scheme was tried on some large, industrial
examples. The results predicted by the theoretical analysis were
confirmed by the outcomes of these examples. We also discuss some
practical issues in choosing the number of bits for the compressed
state representation, along with some of our experiences in
implementing the scheme.