We have developed a tool, called GBT, for verification of systems modeled using graph grammars. The tool performs a symbolic backward reachability analysis to determine if a set of undesirable system configurations is reachable from the initial system configuration.

DYMO is an ad hoc routing protocol, currently on the IETF standards track. An important property for such protocols is that they cannot result in a state in which data packets are forwarded in a loop, never reaching their intended destination. Using GBT, we automatically verify loop freedom of DYMO. The result holds for an arbitrary number of nodes and topology changes.

This is joint work with Mayank Saksena and Bengt Jonsson.