Dr. Walter Guttmann

In diesem Projekt entwerfe ich algebraische Beschreibungen von Berechnungsmodellen für sequentielle Systeme. Ein besonderes Ziel ist es die Vielfalt an bekannten Modellen zu strukturieren und sie zu vereinheitlichen. Dazu gebe ich Axiome für wichtige Aspekte der Modelle an, zum Beispiel für die unendlichen Abläufe einer Berechnung.

• Einige Axiome gelten in vielen Modellen. Sie reichen oft aus um komplexe Ergebnisse herzuleiten, zum Beispiel Programmtransformationen und Verfeinerungsregeln für die Programmentwicklung.
• Einzelne Modelle werden durch das Hinzufügen spezifischer Axiome zu den gemeinsamen charakterisiert. Dadurch spezialisieren sich die Theorien und Methoden für unterschiedliche Anwendungen.

Gemäß den vorausgesetzten Axiomen entsteht eine Hierarchie von algebraischen Strukturen, die Algebras of Computing.

Die Theorien sind durch Axiome erster Ordnung beschrieben, die sich ideal für automatische Beweiser und SMT-Löser eignen. Ich implementiere sie in Isabelle auf der Grundlage von zusammen mit Georg Struth (Sheffield) und Tjark Weber (Cambridge) entwickelten algebraischen Theorien. Gemeinsam wenden wir die Theorien für automatische Beweisführung bei der Programmentwicklung an.

• Algebras for Iteration and Infinite Computations (Isabelle-Theorie für Iterationen und Berechnungsmodelle mit abbrechenden, endlichen und unendlichen Abläufen)
• Unifying Correctness Statements (Isabelle-Theorie einheitlicher Vorbedingungen, Korrektheitsaussagen und -kalküle für mehrere sequentielle Berechnungsmodelle; als PDF)
• Unifying Lazy and Strict Computations (Isabelle-Theorie mit einheitlicher Semantik für Rekursion und Iteration in strikten und nichtstrikten Berechnungsmodellen; als PDF)
• Isabelle-Theoriesammlung für relationale und algebraische Methoden (Georg Struths Seite)

General Correctness: Algebraische Grundlagen und Automatisierung
DAAD Postdoc-Forschungsstipendium für die Universität Sheffield, April 2010 - März 2011

• Extended Designs Algebraically, SCP 78(11):2064-2085, 2013
• Unifying Lazy and Strict Computations, RAMiCS 2012
• Algebras for Iteration and Infinite Computations, Acta Informatica 49(5):343-359, 2012
• Typing Theorems of Omega Algebra, JLAP 81(6):643-659, 2012
• Unifying Correctness Statements, MPC 2012
• Automating Algebraic Methods in Isabelle (mit G. Struth, T. Weber), ICFEM 2011
• Fixpoints for General Correctness, JLAP 80(6):248-265, 2011
• A Repository for Tarski-Kleene Algebras (mit G. Struth, T. Weber), ATE 2011
• Towards a Typed Omega Algebra, RAMiCS 2011
• Unifying Recursion in Partial, Total and General Correctness, UTP 2010
• Partial, Total and General Correctness, MPC 2010
• General Correctness Algebra, RelMiCS/AKA 2009
• ... alle Veröffentlichungen