Syntaktische und semantische Analyse von
Hyperkantenersetzungsgrammatiken zur Heapabstraktion

---

Unendliche Datenstrukturen sind im Allgemeinen durch Model Checking nur
schwer zu handhaben. Das Juggrnaut-Framework implementiert einen Ansatz,
unendliche Datenstrukturen als Hypergraphen zu modellieren und mithilfe
von Hyperkantenersetzungen zu Abstrahieren. Eine Datenstruktur wird dazu
in Form einer Grammatik spezifiziert.

Die genutzte Formalisierung wird in dieser Arbeit aufgearbeitet und die
vom Benutzer eingegebene Grammatik auf die von dieser Formalisierung
geforderten Eigenschaften geprüft. Das Ziel war eine einfache Sprache
zur Spezifikation zu entwickeln sowie hilfreiche Fehlermeldungen bei
möglichen Fehlern auszugeben. Der dabei erstellte Mechanismus zum
Einlesen der Grammatik und der anschließenden Fehlerüberprüfung ist
dabei flexibel genug, um in Zukunft angepasst werden zu können.set of embeddings and give an overview of the time complexity of this approach.