MOVES Seminar 13. Okt, 2011, 11:00

Automata-Based Detection of Hypergraph Embeddings


The verification of programs using pointers and dynamic data structures requires to deal with potentially infinite state spaces. Because of that, it is reasonable to use abstraction techniques capable of dealing with those potentially infinite structures. The Juggrnaut framework applies hyperedge replacement grammars to dynamically abstract and concretize parts of the heap. Abstraction is done by the backwards application of grammars rules, which is related to subgraph isomorphism and therefore NP-complete.


After briefly presenting the basic concepts of heap representation and abstraction using hypergraphs and hyperedge replacement grammars, an automata model is introduced that is able to detect embeddings of grammar rules with certain properties efficiently. Then, I provide a method to construct automata for a given set of embeddings and give an overview of the time complexity of this approach.