Christian Stein

 

Das Dependency Pair Framework zur automatischen Terminierungsanalyse von Termersetzung modulo Gleichungen

 

Diplomarbeitsvortrag

 

Abstract: 

Termersetzungssysteme sind eine bekannte Form der Spezifikation von
Programmen, um die Verifikation von Programmen automatisiert
durchzuführen. Wenn wir bestimmte Eigenschaften von Funktionen des
Programms, wie z.B. die Kommutativität, modellieren wollen, fügen wir
diese in Form von Gleichungen dem Termersetzungssystem hinzu und
betrachten die Termersetzung modulo Gleichungen.
Für die automatisierte Terminierungsanalyse von Termersetzungssystemen
ohne Gleichungen ist das Dependency Pair Framework eine der mächtigsten
bekannten Techniken, das verschiedenste Methoden zur
Terminierungsanalyse mithilfe von Dependency Pairs modular kombiniert.
Mit dem Equational Dependency Pair Framework haben wir analog dazu ein
mächtiges Framework zur automatisierten Terminierungsanalyse von
Termersetzung modulo Gleichungen entwickelt.