An Incremental Heap Canonicalization Algorithm

Software model checkers perform heap canonicalization to reduce the state space explored by exploiting the symmetries present in the heap. The only existing heap canonicalization algorithm does not scale to large heaps. This algorithm requires processing large portions of the heap in every transition. This can lead to poor performance when model checking large programs. This paper presents an incremental heap canonlicalization algorithm. This algorithm generates the same canonical representation for all equivalent heap states. However, for small changes to the heap, the incremental algorithm limits the number of objects traversed. This paper describes the algorithm and its implementation in CMC, a C Model Checker.