Die Dozenten der Informatik-Institute der Technischen Universität Braunschweig laden im Rahmen des Informatik-Kolloquiums zu folgendem Vortrag ein.

Prof. Dr. Martin Lange, Elect. Engineering & Comp. Science, University of Kassel, Germany: Ramsey-basierte formale Verifikation

Beginn: 18.02.2015, 16:30 Uhr Ort: TU Braunschweig, Informatikzentrum, Mühlenpfordtstraße 23, 1. OG, Hörsaal M 161 Webseite: http://www.ibr.cs.tu-bs.de/cal/kolloq/2015-02-18-lange.html Kontakt: Prof. Dr.-Ing. Ina Schaefer

Ziel formaler Verifikation ist es, beweisen zu können, dass ein Programm oder System sich an eine Spezifikation bzgl. dessen Verhaltens halten wird. Somit soll fehlerhaftes Programm- verhalten bereits vor dessen Laufzeit ausgeschlossen werden. Formale Verifikation ist im allgemeinen für beliebige Programme und beliebige Spezifikationen unentscheidbar. Gesucht wird deswegen u.a. nach Spezialfällen, in denen dies dennoch möglich ist. In diesem Vortrag stellen wir ein Verfahren vor, mit dem Sprachinklusion zwischen zwei Visibly-Pushdown-Automaten überprüft werden kann. Diese können z.B. benutzt werden, um abstrahiert das Verhalten von rekursiven, reaktiven Programmen zu modellieren. Sprachinklusion zwischen Automaten kann üblicherweise durch Komplementierung gelöst werden. In der Praxis sind solche Verfahren aber oft zu schlecht. Wir stellen hier ein Verfahren vor, welches ohne explizite Komplementierung auskommt, sondern auf der Suche nach bestimmten Elementen in einer (partiellen) endlichen Halbgruppe basiert. Der Beweis, dass dieses Verfahren korrekt ist, basiert dabei auf einem kombinatorischen Resultat, welches als Satz von Ramsey bekannt ist.