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.

This paper argues that graph grammars naturally model dynamic data structures such as lists, trees and combinations thereof. These grammars can be exploited to obtain finite abstractions of pointer-manipulating programs, thus enabling model checking. Experimental results for verifying Lindstrom's variant of the Deutsch–Schorr–Waite tree traversal algorithm illustrate this.