The aim of this thesis is to analyse graph specification frameworks based on type graphs and show their applicability for verification techniques based on formal language theory. In order to specify and analyse the behaviour of dynamically evolving systems it is important to use suitable specification languages which support practical verification methods.
Many concurrent and distributed systems can be modelled by graphs and graph transformation rules. However, graph-like structures introduce an additional level of complexity, compared to rule-based systems where states have either a word or tree structure. In particular, many complex models induce infinite state spaces, such that explicit verification often fails, since this requires the construction of the entire state space. Therefore, it is necessary to also put a focus on abstraction mechanisms.

Graph abstractions are used in many frameworks for over-approximation of graph transformation systems. These frameworks use abstractions that implicitly specify graph languages and there exist various approaches which try to find an abstraction that is fine enough to enable successful verification, but coarse enough to efficiently implement abstract graph rewriting. This work introduces a general framework which can be suitably instantiated, in order to obtain methods usable in practice.

First, a basic graph specification framework based on type graphs is introduced. The framework is subsequently refined to an approach based on weighted type graphs which can be used for termination analysis of graph transformation systems.

Second, it is shown how three different refinements of the basic framework influence decidability, expressiveness and closure properties of type graph specification languages. Among these refinements, multiply annotated type graphs are discussed which build the foundation for graph specification frameworks expressive enough to specify strongest postconditions.

Finally, by exploiting universal properties from category theory, a general framework for abstract object rewriting is introduced in which strongest postconditions can be computed for annotated objects in an arbitrary topos. A concrete instance of the framework, namely the multiply annotated type graph, is implemented in a prototype tool to substantiate the practicability of the framework.