MOVES Seminar 24 Mar, 2011, 10:00
Local Greibach Normal Form for Hyperedge Replacement Grammars
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. To support the required concretisations, we use a normal form for hyperedge replacement grammars as a generalisation of the Greibach Normal Form for string grammars. In this talk I will briefly present hyperedge replacement grammars and the basic heap abstraction idea. Afterwards the details of a local Greibach Normal Form for graph grammars and its construction will be explained in detail.
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. To support the required concretisations, we use a normal form for hyperedge replacement grammars as a generalisation of the Greibach Normal Form for string grammars. In this talk I will briefly present hyperedge replacement grammars and the basic heap abstraction idea. Afterwards the details of a local Greibach Normal Form for graph grammars and its construction will be explained in detail.
