Dynamic Incremental Hashing in Program Model Checking

Although computationaly neglegdible in other domains, the hashing of states can become one of the most expensive operations in software model checking. The reason lies in the potentially large state descriptions that programs expose. In this paper we introduce incremental hashing on large, dynamically changing state vectors that naturally arise during the verification of software in program model checkers. We exploit the fact that only small portions of the state description are changed by a single transition. Based on the changes in the predecessor state, the new state and its hash value can be computed efficiently.