Dynamic Incremental Hashing in Program Model Checking
Tilman Mehler, Stefan Edelkamp · Electronic Notes in Theoretical Computer Science · 2006
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.