Dr. Christian Urban

"Verifikation von Programmiersprachen"

Zusammenfassung: Interaktive Theorembeweiser sind heutzutage gut genug, um die Implementierung von zum Beispiel Compilern oder Micro-Kernel- Betriebssystemen zu verifizieren. Solche Verifikationen bedeuten aber immernoch Projekte von mehreren Mann-Jahren oder Mann- Jahrzehnten. Im Vortrag werde ich Ideen präsentieren, wie derartige Projekte vereinfacht werden können. Dabei werde ich mich auf die Verifikation von Programmiersprachen konzentrieren. In der Praxis verursachen Compiler-Optimierungen und unvorhergesehene Kombinationen von Sprachkonstrukten häufig Fehler. Um diese auszuschließen, muss ein mathematischer Beweis für die Korrektheit der Programmiersprache und der Code-Generierung angegeben werden. Ziel meiner Arbeit ist es, Theorembeweiser so zu verbessern, damit solche Beweise deutlich einfacher werden.