Verifikation von Dafny-Programmen

Typ:	DA
Datum:	05.08.2013
Betreuer:	Daniel Grahl
Aushang:

Software-basierte Systeme halten Einzug in nahezu alle Bereiche unseres Lebens. Allerdings bleibt die Qualität der Software trotz ihrer wachsenden Bedeutung nur allzuoft auf der Strecke. In manchen Bereichen mag dies tolerierbar sein, sobald aber durch fehlerhafte Software Menschenleben gefährdet sind (z. B. Eisenbahnwesen oder Anwendungen in der Medizin) oder hohe finanzielle Schäden zu befürchten sind (z. B. Internet-Banking), muss auf die Qualität – insbesondere auf die Korrektheit – der Software besonderer Wert gelegt werden.

Dafny ist eine experimentelle imperative Programmiersprache, die von K. Rustan M. Leino bei Microsoft Research entwickelt wurde. Dafny wurde mit dem Ziel entworfen, formale Korrektheitsbeweise zu erleichtern. Sie verzichtet daher bewusst auf Features gängiger (objekt-orientierter) Sprachen wie Java, wie etwa Laufzeitfehler, Vererbung oder Nebenläufigkeit. Dafür sind Konzepte wie Methodenverträge oder Invarianten direkt in die Sprache eingebaut. Unter http://rise4fun.com/Dafny kann man Dafny-Programme online laufen lassen ohne einen Interpreter zu installieren.

An unserem Lehrstuhl wird seit über 10 Jahren das KeY-System entwickelt, mit dem Java-Programme formal (d.h. logikbasiert) verifiziert werden. Es arbeitet regelbasiert und verfügt über einen eigenen eingebauten, interaktiven Logikbeweiser. Die Beweisführung in KeY entspricht einer symbolischen Ausführung des Programms und wird dadurch transparent. Im Rahmen dieser Masterarbeit soll erarbeitet werden, wie mit KeY auch Dafny-Programme verifiziert werden können. Dazu gehört die Definition einer Programmlogik (Dynamischer Logik), die Aussagen über Dafny-Programme treffen kann, sowie die Erstellung von Regeln, mit denen diese Aussagen bewiesen werden können.

Die Ausarbeitung in englischer Sprache ist erwünscht. Am Ende der Arbeit sollte eine erste prototypische Implementierung der Beweisregeln in KeY möglich sein. Grundlegende Kenntnisse über Programmiersprachen, insbesondere im Bereich Übersetzerbau, sowie formale Logiken werden vorausgesetzt. Bei Interesse können mögliche Vorarbeiten im Rahmen eine Bachelor-Arbeit oder einer Hiwi-Tätigkeit erledigt werden.