1: \begin{abstract}

2: We propose a new approach to heap analysis through an abstract domain

3: of automata, called \emph{automatic shapes}. The abstract domain uses a particular kind of automata, called \emph{quantified data automata on skinny trees} (\QSDA s), that allows to define universally quantified properties of singly-linked lists.

4: To ensure convergence of the abstract fixed-point computation, we introduce a sub-class of \QSDA s called elastic \QSDA s, which also form an abstract domain.

5: We evaluate our approach on several list manipulating programs and we show that the proposed domain is powerful enough to prove a large class of these programs correct.

6: \end{abstract}

7: