Improved probabilistic verification by hash compaction

Abstract

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.