Logische und softwaretechnische Herausforderungen bei der Verifikationoptimierender Compiler

Abstract

Korrektheit von Compilern ist notwendige Voraussetzung für die Korrektheit der damit übersetzten Software. Insbesondere optimierende Compiler sind oft fehlerhaft. In diesem Papier stellen wir nach einem Überblick über den Stand der Forschung unsere neuen Arbeiten zur Verifikation optimierender Compiler vor. Dabei diskutieren wir zum einen, welche logischen Probleme sich bei der formalen Verifikation von Übersetzungsalgorithmen in Compilern mittels Theorembeweisern ergeben und welche Lösungen wir dafür entwickelt haben. Zum anderen zeigen wir, wie man die Korrektheit auch realer optimierender Compiler mit beträchtlichem Implementierungsumfang sicherstellen kann. Damit tragen unsere Ergebnisse zur Korrektheit von Compilern, einem wichtigen Werkzeug in der Softwaretechnik, bei. Außerdem entwickeln wir auf diese Weise Methoden, die auch in anderen Anwendungsbereichen zur Verifikation von Software eingesetzt werden können.