Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
An Incremental Heap Canonicalization Algorithm

Madanlal Musuvathi and David L. Dill

Abstract

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.

Details

Publication typeTechReport
NumberMSR-TR-2004-37
Pages0
InstitutionMicrosoft Research
> Publications > An Incremental Heap Canonicalization Algorithm