MOVES Seminar 5 Sep 2008

Abstracting Complex Data Structures by Hyperedge Replacement

 

Stefan Rieger

 

We present a novel application of hyperedge replacement grammars,
showing that they can serve as an intuitive formalism for abstractly
modeling dynamic data structures. The aim of our framework is to extend
finite-state verification techniques to handle pointer-manipulating
programs operating on complex dynamic data structures that are
potentially unbounded in their size. The idea is to represent both
abstraction mappings on user-defined dynamic data structures and the
(abstract) semantics of pointer-manipulating operations using graph
grammars, supporting a smooth integration of the two aspects. We
demonstrate how our framework can be employed for analysis and
verification purposes, e.g., to prove that a procedure preserves
structural invariants of the heap.