Cooperation with
Mooly Sagiv (Tel Aviv University) and
Thomas Reps (University of Wisconsin in Madison)
This project concerns the static analysis of programs
that perform destructive updating on heap-allocated storage.
It addresses problems
that can be looked at as
- pointer-analysis,
- alias-analysis,
- sharing-analysis,
- storage-analysis aka shape-analysis, or
- type-checking problems.
We will choose the term shape-analysis in the following.
Shape anlaysis tries to give for each program point
a conservative, finite characterization of the possible shapes
that the program's heap allocated data structures can have at that point.
For certain programs our analysis is able to detect that
- when the input to the program is an (acyclic) singly linked list,
the output is also an (acyclic) singly linked list,
- when the input to the program is a doubly linked list,
the output is also a doubly linked list,
- when the input to the program is a tree,
the output is also a tree.
A presentation of the Shape Analysis (Invited Talk from CC 2000) can be found
here (53 slides), all other
publications can be found here.
|