Verification of program computations

Abstract

Formal verification of complex algorithms is challenging. Verifying their implementations in reasonable time is infeasible using current verification tools and usually involves intricate mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm -- yet it is all the user has to trust. The verification of checkers is feasible with current tools and leads to computations that can be completely trusted. We describe a framework to seamlessly verify certifying computations. We demonstrate the effectiveness of our approach by presenting the verification of typical examples of the industrial-level and widespread algorithmic library LEDA. We present and compare two alternative methods for verifying the C implementation of the checkers. Moreover, we present work that was done during an internship at NICTA, Australia's Information and Communications Technology Research Centre of Excellence. This work contributes to building a feasible framework for verifying efficient file systems code. As opposed to the algorithmic problems we address in this thesis, file systems code is mostly straightforward and hence a good candidate for automation.

Die formale Verifikation der Implementierung komplexer Algorithmen ist schwierig. Sie übersteigt die Möglichkeiten der heutigen Verifikationswerkzeuge und erfordert für gewöhnlich komplexe mathematische Theoreme. Zertifizierende Algorithmen berechnen zu jeder Ausgabe ein Zerfitikat, das die Korrektheit der Antwort bestätigt. Ein Checker für ein solches Zertifikat ist normalerweise ein viel einfacheres Programm und doch muss ein Nutzer nur dem Checker vertrauen. Die Verifizierung von Checkern ist mit den heutigen Werkzeugen möglich und führt zu Berechnungen, denen völlig vertraut werden kann. Wir beschreiben eine Rahmenstruktur zur Verifikation zertifizierender Berechnungen und demonstrieren die Effektivität unseres Ansatzes an Hand typischer Beispiele aus der hochqualitätiven und oft eingesetzten LEDA Algorithmenbibliothek. We präsentieren und bewerten zwei alternative Methoden zur Verifikation von Checkerimplementierungen in C. Desweiteren beschreiben wir Ergebnisse, die während eines Praktikums am NICTA, dem Australischen Forschungszentrum für Informations- und Kommunikationstechnik, erzielt wurden. Diese Arbeit trägt zum Aufbau einer praktisch einsetzbaren Rahmenstruktur zur Verifizierung von Code für effiziente Dateisysteme bei. Im Gegensatz zu den algorithmischen Problemen, die wir in dieser Arbeiten behandeln, ist der Code für Dateisysteme weitgehend unkompliziert unddaher ein guter Kandidat zur Automatisierung.