Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
Pranav Garg, P. Madhusudan, Gennaro Parlato

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Formal Methods in Verification · Logic, programming, and type systems
