On the Expressive Power of Canonical Abstraction

Abstraction and abstract interpretation are key tools for automatically verifying properties of systems. One of the major challenges in abstract interpretation is how to obtain abstractions that are precise enough to provide useful information. In this talk, I will survey a parametric abstract domain called canonical abstraction which was motivated by the shape analysis problem of determining “shape invariants” for programs that perform destructive updating on dynamically allocated storage. The shape analysis problem was originally defined by [1]. Canonical abstraction was originally defined in [2]. A system for abstract interpretation based on abstract interpretation was defined in [3,4].I will discuss properties that have been verified using this abstraction. A couple of interesting properties of this abstract domain will be presented. Finally, I will also show some of the limitations of this domain.