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

TL;DR

This paper introduces quantified data automata on skinny trees (QSDAs) as an abstract domain for heap analysis, enabling the verification of universally quantified properties of singly-linked lists in programs.

Contribution

It presents a novel automata-based abstract domain for list analysis, including elastic QSDAs for ensuring convergence, and demonstrates its effectiveness on list-manipulating programs.

Findings

Successfully proved correctness of several list programs

Powerful enough to handle a large class of list properties

Introduced elastic QSDAs for fixed-point convergence

Abstract

We propose a new approach to heap analysis through an abstract domain of automata, called automatic shapes. The abstract domain uses a particular kind of automata, called quantified data automata on skinny trees (QSDAs), that allows to define universally quantified properties of singly-linked lists. To ensure convergence of the abstract fixed-point computation, we introduce a sub-class of QSDAs called elastic QSDAs, which also form 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.