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.
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.

