An analysis of bitstate hashing

Abstract

The bitstate hashing, or supertrace, technique was introduced in 1987 as a method to increase the quality of verification by reachability analyses for applications that defeat analysis by traditional means because of their size. Since then, the technique has been included in many research verification tools, and was even adopted in some tools that are marketed commercially. It is therefore important that we understand well how and why the method works, what its limitations are, and how it compares with alternative schemes that attempt to solve the same problem. The original motivation for the bitstate hashing technique was based on empirical evidence of its effectiveness. In this paper we provide the analytical argument. We compare the technique with two alternatives that have been proposed in the recent literature as potential improvements.