Heapabstraktion durch partielle Graphreduktion mittels Graphgrammatiken  (Diplomarbeitsvortrag)

 

 

Ralf Grossmann

 

Abstract

 

Heapbasierte dynamische Datenstrukturen sind in heutigen Programmen weit
verbreitet und stellen eine Herausforderung f?r die
Verifikation dar. Zur Vermeidung unendlicher Zustandsr?ume bei ihrer Analyse ist
eine Abstraktion der Datenstrukturen notwendig.
Durch eine Darstellung des Heaps als Hypergraph und die r?ckw?rtige
Regelanwendung einer entsprechend angepassten Graphgrammatik
realisieren wir im vorgestellten Verfahren diesen Abstraktionsschritt. Umgekehrt
werden Ableitungsschritte der Grammatik
eingesetzt, um bei Bedarf eine passende Konkretisierung des Heaps zu
erm?glichen. Im Laufe des Vortrags entwickeln wir
schrittweise geeignete Grammatiken f?r Datenstrukturen wie beispielsweise bin?re
B?ume mit verbundener Blattfront. Zudem wird ein
Endlichkeitstest f?r die Analyse vorgestellt und wir betrachten die Ergebnisse,
die dieser f?r die zuvor ermittelten Grammatiken
liefert.