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.

- Shape information can be used to execute tasks in parallel when they are guaranteed to access disjoint pieces of memory.
- In C programs shape analysis can be used to prove the absence of memory leaks and to identify memory leaks (e.g., see Checking Cleanness in Linked Lists, Nurit Dor, Michael Rodeh, Shmuel Sagiv, leanness in Linked Lists. SAS 2000: 115-134)
- It can also be used to automatically reclaim memory which cannot be used (e.g., see Establishing local temporal heap safety properties with applications to compile-time memory management. Ran Shaham, Eran Yahav, Elliot K. Kolodner, Mooly Sagiv. Sci. Comput. Program. 58(1-2): 264-289 (2005) and Uniqueness inference for compile-time object deallocation. Sigmund Cherem, Radu Rugina: ISMM 2007: 117-128)
- It can be used to prove partial correctness of library functions. For instance it can be used to ensure that a sort method correctly sorts a list (see putting static analysis to work for verification: A case study. Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm. ISSTA 2000: 26-38)
- It can be used for proving properties of concurrent programs such as absence of deadlocks and mutual exclusion. (e.g., see Eran Yahav, Mooly Sagiv Verifying safety properties of concurrent heap-manipulating programs. ACM Trans. Program. Lang. Syst. 32(5): (2010))
- It can be used to prove termination of programs.
For example to show that a loop of the form
**"for (p=x; p !=y, p = p.next)**" terminates, one needs to show that there must be a 'next'-path in the heap between the element pointed-to by 'x' to the element pointed-to by 'y'.

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.

- The TVLA homepage (outdated)
- The Separation Logic Homepage
- SLAyer: Automatic formal verification for programs with heaps
- The Xisa Analyzer
- Jackalope Heap Analysis Toolkit
*Ahmed Boujjani's group at University Paris 7* - The Safe project at the Technion