Verifying Graph Programs with Monadic Second-Order Logic

To verify graph programs in the language GP 2, we present a monadic second-order logic with counting and a Hoare-style proof calculus. The logic has quantifiers for GP 2's attributes and for sets of nodes or edges. This allows to specify non-local graph properties such as connectedness, k-colourability, etc. We show how to construct a strongest liberal postcondition for a given graph transformation rule and a precondition. The proof rules establish the total correctness of graph programs and are shown to be sound. They allow to verify more programs than is possible with previous approaches. In particular, many programs with nested loops are covered by the calculus.