Projektstart: 01.04.2011

Laufzeit: 2 + 2 Jahre

Projektträger: DFG (Deutsche Forschungsgemeinschaft)

Projektverantwortung vor Ort: Prof. Dr. Bernhard Möller

Beteiligte WissenschaftlerInnen der Universität Augsburg: Han-Hing Dang, Dr. Martin E. Müller

Beteiligte WissenschaftlerInnen / Kooperationen: Sir Tony Hoare (Microsoft Research), Prof. Peter O'Hearn (Queen Mary, University of London), Dr. Peter Höfner (NICTA Australia), Rasmus Lerchedahl Petersen (Queen Mary, University of London), Prof. Dr. Georg Struth (University of Sheffield), John Wickerson (Computer Laboratory, University of Cambridge)

Zusammenfassung

Seit etwa 40 Jahren versucht man die Korrektheit von Programmen mittels formaler Methoden sicherzustellen. Da die Kalküle von Hoare und Dijkstra keine Ausdrucksmittel für komplexe, speziell verzeigerte, Datenstrukturen enthalten, wurden sie in den letzten Jahren von Reynolds, O'Hearn und anderen zur Separationslogik weiterentwickelt. Diese bezieht inzwischen auch Parallelität und gemeinsam benutzte Datenstrukturen mit ein. Die meisten der genannten Kalküle sind durch so genannte "special-purpose" Beweissysteme computerunterstützt, d.h., es wird versucht Eigenschaften automatisch herzuleiten. Der Nachteil dieser Systeme ist, dass sie für jeden neuen Kalkül eigens entwickelt werden müssen. Diese Vorgehensweise ist mühsam, kosten- und zeitintensiv.
Hier setzt die Idee der Algebraisierung an. Durch Abstraktion erlaubt sie oft das formale Schließen mittels einfacher Gleichungsgesetze, wie sie aus der Schulalgebra bekannt sind. Diese können direkt in bereits vorhandene vollautomatische Beweissysteme eingegeben werden, so dass nicht für jedes Anwendungsfeld ein neues Beweissystem zu erstellen ist. Das Projektziel ist, aufbauend auf einem bereits vorhandenen Grundstock, eine algebraische Darstellung separationslogischer Kalküle. Hierbei liegt das Hauptaugenmerk auf der algebraischen Charakterisierung und deren Verwendung für Verifikationsaufgaben. Als positiver Nebeneffekt soll genützt werden, dass durch Algebraisierung Verifikationsaufgaben mittels bereits vorhandener Beweissysteme durchgeführt werden können.