Graphen sind ein vielseitiges Werkzeug zur Modellierung von Systemzuständen. Ich konzentriere mich auf zwei Systemklassen, Netzwerktopologien und Programmheaps, in denen sowohl die Knotenanzahl als auch die Kanten zwischen Knoten dynamisch und unbeschränkt sind. Diese Arbeit behandelt die Modellierung, Analyse und Verifikation solcher Systeme. Anspruchsvolle Fallstudien wie Linux-Kernel-Datenstrukturen und automatische Verkehrkontrollsysteme werden bearbeitet, wobei Techniken aus der statischen Programmanalyse, Graphersetzungssystemen, Shape Analyse und Verifikation von Systemen mit unendlichen Zustandsräumen zum Einsatz kommen. Alle verwendeten Techniken, Tricks und Heuristiken werden zu einer Werkzeugkiste für graph-basierte Modellierung, Analyse und Verifikation kombiniert.     «

Graphen sind ein vielseitiges Werkzeug zur Modellierung von Systemzuständen. Ich konzentriere mich auf zwei Systemklassen, Netzwerktopologien und Programmheaps, in denen sowohl die Knotenanzahl als auch die Kanten zwischen Knoten dynamisch und unbeschränkt sind. Diese Arbeit behandelt die Modellierung, Analyse und Verifikation solcher Systeme. Anspruchsvolle Fallstudien wie Linux-Kernel-Datenstrukturen und automatische Verkehrkontrollsysteme werden bearbeitet, wobei Techniken aus der statischen...     »