The purpose of shape analysis is to infer properties about unbounded data structures, such as trees or lists. We will present a shape analysis based on abstract inerpretation, which uses separation logic and inductive definitions. Our analysis targets C programs. The elements of our abstract domain can be seen as separation logic formulae or equivalently as separating shape graphs. It is parametric in the inductive definitions of the structures ti be used for a given analysis.

We will present the definition of this abstract domain together with the main analysis algorithms such as materialization (local concretization) and widening (global abstraction) and our recent progress for accomodating low level aspects of the C language.