Antrittsvorlesung von Prof. Dr. Roland Meyer Von der Grundlagenkrise zur Programmanalyse

Prof. Dr. Roland Meyer, Institut für Theoretische Informatik der Technischen Universität Braunschweig, hält seine Antrittsvorlesung „Von der Grundlagenkrise zur Programmanalyse“ am

Mittwoch, 22. November 2017, um 17 Uhr,
Aula, Pockelsstraße 11, Haus der Wissenschaft, 38106 Braunschweig.

 Die Grundfesten der Mathematik wurden 1903 von Bertrand Russell mit dem Barbier von Sevilla erschüttert. Dieser Barbier rasiert die Männer des Ortes, die sich nicht selbst rasieren, doch wer rasiert den Barbier? Die Antwort ist, dass der Barbier nicht existieren kann. Auf die Mathematik übertragen ist nicht einmal der grundlegende Begriff einer Menge, formuliert als Ansammlung unterschiedlicher Objekte, wohldefiniert – eine Einsicht, die die Mathematik in die sogenannte Grundlagenkrise stürzte. Um derartige Paradoxa zu vermeiden, schlug David Hilbert 1920 vor, die zur Herleitung einer Aussage als gültig angenommenen Axiome und Schlussregeln explizit anzugeben. Eine Aussage gelte als bewiesen, wenn sie sich in dem entsprechenden formalen System ableiten ließe.

Doch ist es möglich, automatisch wahre mathematische Aussagen zu finden? Alan Turing machte diese Hoffnung schon 1936 zunichte. Er zeigte, dass sich für allgemeine Funktionen wichtige Eigenschaften nicht automatisch nachweisen lassen. Funktionen werden dabei als Rechenverfahren aufgefasst, als Algorithmen, später (Computer)programme genannt.

Mit der Entwicklung des Computers hat sich in den kommenden Jahrzehnten zweierlei gezeigt. In beschränktem Rahmen lassen sich durchaus Informationen über Funktionen berechnen. Das Erstellen von Funktionen in der Form von Programmen ist eine fehleranfällige Tätigkeit, es besteht daher Bedarf an Analyseverfahren, die ein Programm als Eingabe entgegennehmen und automatisch dessen Korrektheit prüfen. Diesem Forschungsgebiet widmet sich das Institut für Theoretische Informatik der TU Braunschweig mit dem Ziel, Alan Turings theoretisch gesteckte Grenzen hinter die praktische Nutzbarkeit zu verschieben.

Zur Person

Roland Meyer studierte von 2001 bis 2005 an der Universität Oldenburg Informatik und Mathematik. Im Anschluss promovierte er 2009 in Oldenburg mit einer Dissertation über rekonfigurierbare Systeme. Es schloss sich eine Forschungstätigkeit auf dem Gebiet Verifikation im LIAFA, Laboratoire d’Informatique Algorithmique, Paris, an. Von 2010 bis 2016 hatte er eine Professor für Theoretische Informatik an der TU Kaiserslautern. Seit 2016 ist Roland Meyer Professor für Theoretische Informatik an der Technischen Universität Braunschweig.