Technical Report No.109 - Abstract

Juergen Eckerle, Thomas Lais
New Methods for Sequential Hashing with Supertrace

Partial search methods like bitstate hashing, or supertrace, allow formal verification techniques to be applied to problems which normally could not be solved by exhaustive verification. A high coverage (defined as the percentage of the reachable states actually explored by the verifier) is important since the higher the coverage the lower the probability that a protocol error is not detected. In literature sequential hashing is proposed to improve the coverage of supertrace (i.e. start repeatedly supertrace by using different hash functions). Since supertrace is included in many commercial and noncommercial verification tools, it is important to know where its limitations are and where there is potential for possible improvements. We present both theoretical and experimental results to measure the quality of multiple hashing with supertrace. Tests made with the SPIN validator with different classes of hash functions show that the additional number of states reached in successive runs decreases rapidly. A coverage of close to 1 is practically impossible. While all the hash functions have the same asymptotical behaviour universal hashing seems to be best. We present an analysis for the expected coverage of sequential hashing which explains accurately the experimental results. Our new mathematical model shows that the overlap of successive runs is much higher than predicted by former approaches. Additionally, it predicts that simple randomization strategies which in successive runs change randomly both, the hash function and the traversal order of the states can increase the coverage sibnificantily. Experimental results show that our new algorithm, universal supertrace, which is based on such randomization techniques, outperforms the original supertrace and allows the coverage to be increased by a factor of up to 9-10.