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, 威尼斯赌博游戏_威尼斯赌博app-【官网】 of London), Dr. Peter H?fner (NICTA Australia), Rasmus Lerchedahl Petersen (Queen Mary, 威尼斯赌博游戏_威尼斯赌博app-【官网】 of London), Prof. Dr. Georg Struth (威尼斯赌博游戏_威尼斯赌博app-【官网】 of Sheffield), John Wickerson (Computer Laboratory, 威尼斯赌博游戏_威尼斯赌博app-【官网】 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.