Graph-Based Shape Analysis Beyond Context-Freeness
Abstract
We develop a shape analysis for reasoning about relational properties of data structures. Both the concrete and the abstract domain are represented by hypergraphs. The analysis is parameterized by user-supplied indexed graph grammars to guide concretization and abstraction. This novel extension of context-free graph grammars is powerful enough to model complex data structures such as balanced binary trees with parent pointers, while preserving most desirable properties of context-free graph grammars. One strength of our analysis is that no artifacts apart from grammars are required from the user; it thus offers a high degree of automation. We implemented our analysis and successfully applied it to various programs manipulating AVL trees, (doubly-linked) lists, and combinations of both.
Cite
@article{arxiv.1705.03754,
title = {Graph-Based Shape Analysis Beyond Context-Freeness},
author = {Hannah Arndt and Christina Jansen and Christoph Matheja and Thomas Noll},
journal= {arXiv preprint arXiv:1705.03754},
year = {2018}
}