Algebraische Kalküle für Separationslogik

• Antragsteller: Professor Dr. Bernhard Möller
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2011 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 188417285

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.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Großbritannien
• Beteiligte Person: Professor Tony Hoare