Quantified data automata on skinny trees: An abstract domain for lists

Pranav Garg, P. Madhusudan, Gennaro Parlato

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 20th International Symposium, SAS 2013, Proceedings
Pages172-193
Number of pages22
DOIs
StatePublished - 2013
Event20th International Static Analysis Symposium, SAS 2013 - Seattle, WA, United States
Duration: Jun 20 2013Jun 22 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7935 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other20th International Static Analysis Symposium, SAS 2013
CountryUnited States
CitySeattle, WA
Period6/20/136/22/13

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Quantified data automata on skinny trees: An abstract domain for lists'. Together they form a unique fingerprint.

Cite this