In program analysis, a shape analysis is a static code analysis technique that discovers and verifies properties of linked, dynamically allocated data structures in (usually imperative) computer programs. For example, discriminating between cyclic and acyclic lists and proving that two data structures cannot access the same piece of memory.
As part of the shape analysis research our group developed TVLA, which was used to prove interesting properties of programs manipulating unbounded data structures.
The shape analysis problem becomes more interesting in concurrent programs that manipulate pointers and dynamically allocated objects. Moreover, new threads can also be generated. This problem was addressed in the Phd thesis of Eran Yahav.
Another interesting aspect of shape analysis is the interaction between the heap and procedure calls which was addressed in the Phd thesis of Noam Rinetzy.
Scaling shape analysis to large programs is a challenging task. The abstractions that developed in the past represent the heap in a uniform fashion. In his PhD thesis Roman Manevich develops an abstraction which decomposes the heap into subheaps and abstract away the correlations between the subheaps. This allows applying the shape analysis to more complex programs. Roman and Tal Lev-Ami developed a system called HeDec and applied it to prove linearizability of concurrent fine-grained data structure implementations in a scalable way.
The problem of reasoning about shapes is interesting both for automatic and semi-automatic verification. Tal Lev-Ami, Neil Immerman, Tom Reps, Siddharth Srivastava, Greta Yorsh, and myself showed that one can reason about recahability using pure first order logic. Greta also showed that theorem provers can be used to compute transformers for shape analysis.
The shape analysis problem was originally formulated by Neil Jones and Steven Muchnick in 1981. I started looking into the problem in 1995 together with Tom Reps and Reinhard Wihelm. Back then, the problem was considered difficult and non-interesting. Following our research, the problem became fashionable with many excellent results cited below.