Peter Hawkins, Stanford University


Hierarchical Shape Graphs

Despite extensive research on methods for modeling memory in static
analysis, the problem of automatically proving memory-safety of
systems code is largely open. Proving safety of low-level code
requires extensive information about the structure of memory, but
analyses with the right combination of precision, scalability, and
simplicity are yet to be developed. In this talk we introduce the
Hierarchical Shape Graph, which is a new abstract representation of
memory that generalizes points-to graphs, and that allows us to
describe common nested data structures in a succinct and natural way.
We argue that our graphical representation is not only a simple and
intuitive way to depict the layout of memory, but can also form the
basis of a powerful shape analysis system. In particular, our shape
analysis built using this representation is capable of automatically
proving strong safety properties of complex list manipulation routines
taken from real systems code, for example that a destructive mergesort
of a doubly-linked list produces a doubly-linked list as output.

Joint work with Kathleen Fisher and Alex Aiken.