Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists

We propose a new approach to heap analysis through an abstract domain of automata, called automatic shapes. Automatic shapes are modeled after a particular version of quantified data automata on skinny trees (QSDAs), that allows to define universally quantified properties of programs manipulating acyclic heaps with a single pointer field, including data-structures such singly-linked lists. To ensure convergence of the abstract fixed-point computation, we introduce a subclass of QSDAs called elastic QSDAs, which forms an abstract domain. 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.