Seminar 30 July 11:00, 2012

Inferring Heap Abstraction Grammars

 

Heap abstraction grammars have successfully been used in the past to extend traditional model-checking techniques to pointer programs. The downside of this approach is that it requires the user to specify such a grammar for every program that is to be checked. In this work we first give a brief introduction to hypergraphs, heap abstraction grammars and how they are used for modeling heap configurations. We then present an algorithm that observes some runs of a given program and produces a heap abstraction grammar that describes the behavior of this program on the heap in the most concise way, using techniques from the field of machine learning. We also take into account simple recursive data structures. Subsequently we present the results of some experiments with an implementation of this algorithm using the Juggrnaut-framework and conclude with a brief outlook on possible improvements of grammatical inference.