Die Lösung der POPLMARK-Challenge: Neue Techniken zur maschinellen Verifikation der Korrektheit von Programmiersprachen

• Antragsteller: Dr. Christian Urban
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2006 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 18284775

Die Korrektheit von Programmiersprachen ist extrem schwierig sicherzustellen: unvorhergesehene Kombinationen von bestimmten Sprachkonstrukten verursachen oft Fehler. Leider kann ein einziger Fehler in einer Programmiersprache drastische Konsequenzen haben. Zum Beispiel wurde in der Spezifikation der weit verbreiteten Programmiersprache JAVA ein Fehler gefunden, den ein böswilliger Programmierer ausnutzen kann, um Unheil auf einem Computer oder in einem Netzwerk anzurichten [22]. Um sicherzustellen, dass die Spezifikation einer Programmiersprache korrekt ist, muss ein mathematischer Beweis für die Verifikation der Korrektheit angegeben werden. Mein Vorhaben ist es, die POPLMARK-Challenge zu lösen. Die von mehreren Wissenschaftlern der Pennsylvania Universität und der Universität in Cambridge aufgestellte Herausforderung besagt [2]: To gauge progress in this area, we issue here a set of challenge problems, dubbed the POPLMARK-Challenge, chosen to exercise many aspects of programming languages that are known to be very difficult to formalize. Die POPLMARK-Challenge ist die zur Zeit spannendste und zukunftsweisendste Herausforderung auf dem Gebiet der maschinellen Deduktion. Aufgrund meines neuartigen Arbeitsansatzes und meiner Vorarbeiten wird dieses Projekt es ermöglichen, leichter mathematische Beweise über Programmiersprachen in Theorembeweisern zu führen.Mit existierenden Techniken ist dies unmöglich. Obwohl die Motivation für das Projekt die POPLMARK-Challenge ist, werden die Ergebnisse wichtige Basistechnologien für Theorembeweiser im Allgemeinen liefern. Denn über die Herausforderung hinaus möchte ich erreichen, dass maschinelle Beweise über jedwede Art von mathematischer Syntax bequem von Nicht-Experten (auf dem Gebiet der maschinellen Deduktion) geführt werden können. Es soll damit prinzipiell möglich werden, dass alle erscheinenden Artikel über mathematische Syntax, also auch Artikel über Programmiersprachen, mit elektronischen Anhängen versehen werden können, in welchen die Beweise maschinell überprüft wurden. Dadurch könnten Fehler grundsätzlich ausgeschlossen werden.

• DFG-Verfahren: Emmy Noether-Nachwuchsgruppen