Juggrnaut - A Graph-Based Approach to Heap Abstraction

Christina Jansen

Heap-based data structures play an important role in modern programming concepts. However standard verification algorithms cannot cope with infinite state spaces as induced by these structures. A common approach to solve this problem is to apply abstraction techniques. We use hyperedge replacement grammars for this purpose as their production rules can be used to partially abstract and concretise heap structures. In order to provide a robust abstraction approach the grammars have to fulfill additional properties, e.g. ensuring that each abstract state represents at least one concrete and valid heap.

In this talk I will briefly present hyperedge replacement grammars and the heap abstraction idea based on graph grammars including the necessary properties. As there exists a strong connection between hyperedge replacement grammars and separation logic (established by M. Dodds) similar properties can be derived in the context of separation logic. We will discuss their preservation under the transformation between formulae and graph grammars. Furthermore I will give a short overview of our heap abstraction framework "Juggrnaut" as well as some experimental results.