# Graph-Based Shape Analysis Beyond Context-Freeness

## TL;DR

This paper introduces a novel shape analysis framework using hypergraphs and extended graph grammars to reason about complex data structures like balanced trees with minimal user input.

## Contribution

It extends context-free graph grammars to model complex data structures and provides an automated analysis tool that requires only user-supplied grammars.

## Key findings

- Successfully analyzed AVL trees, lists, and their combinations.
- Automated analysis with minimal user artifacts.
- Capable of modeling complex data structures like balanced trees.

## 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.