Verifying pointer programs using graph grammars

摘要

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.