An Incremental Heap Canonicalization Algorithm

Abstract. The most expensive operation in explicit state model checking is the hash computation required to store the explored states in a hash table. One way to reduce this computation is to compute the hash incrementally by only processing those portions of the state that are modified in a transition. This paper presents an incremental heap canonicalization algorithm that aids in such an incremental hash computation. Like existing heap canonicalization algorithms, the incremental algorithm reduces the state space explored by detecting heap symmetries. On the other hand, the algorithm ensures that for small changes in the heap the resulting canonical representations differ only by relatively small amounts. This reduces the amount of hash computation a model checker has to perform after every transition, resulting in significant speedup of state space exploration. This paper describes the algorithm and its implementation in two explicit state model checkers, CMC and Zing.

• Type: Conference
• Year: 2005
• Where: SPIN
• Authors: Madanlal Musuvathi, David L. Dill
• Keywords: Explicit State Model, Hash Computation, Heap Canonicalization Algorithms, SPIN 2005, Theoretical Computer Science