MOVES/Zwischenvortrag zur Diplomarbeit, 24 Sep 2009, 11:00

Christina Jansen

Von der Hyperkantenersetzungsgrammatik zur Heapabstraktionsgrammatik

 

MOVES/Zwischenvortrag zur Diplomarbeit

 

Abstract:

 

Für eine Nutzung von Hyperkantenersetzungsgrammatiken (HRGs) zur Verifikation von heapbasierten dynamischen Datenstrukturen ist es wünschenswert, eine problembezogene, geeignete HRG automatisch erstellen zu können. Diese muss verschiedene notwendige Eigenschaften besitzen, um die Korrektheit des Verifikationsprozesses im Juggrnaut-Framework gewährleisten zu können. Eine diese Eigenschaften erfüllende HRG nennt man dann Heapabstraktionsgrammatik.

 

In diesem Zwischenvortrag zur Diplomarbeit wird ein Überblick über die notwendigen Anforderungen an eine HRG gegeben, die als Ausgangspunkt für den Verifikationsprozess dient. Desweiteren wird daran anknüpfend die Konstruktion einer Heapabstraktionsgrammatik zu einer gegebenen HRG erläutert.