Verifying pointer programs using graph grammars ?
We propose to employ graph grammars for modelling dynamic data structures. Typical examples include lists, trees and combinations thereof. We show how to obtain finite state-space abstractions of heap-manipulating programs. This enables the application of standard model checking techniques. We report on the automated verification of a stackless tree traversal algorithm.
verification dynamic data structures hyperedge replacement grammars java bytecode