Ich bin nach Berlin gezogen.

Am Lehrstuhl habe ich das DFG Projekt „Verifikation von SPS-Programmen mittels Model-Checking und statischer Analyse“ bearbeitet. Speicherprogrammierbare Steuerungen (SPSen) sind Steuerungscomputer zur Automatisierung, Regelung und Steuerung von großtechnischen Anlagen und Maschinen. In diesem Projekt geht es darum, mittels formaler Methoden Fehler in SPS-Programmen zu finden oder zu beweisen, dass sie ihre Spezifikation erfüllen. Insbesondere ist es dazu nötig, geeignete Abstraktion-Techniken zu entwickeln, die es erlauben, Berechnungsschritte auf einer großen Menge von Werten gleichzeitig auszuführen. Erst so ist es möglich, die Analysen auf größere SPS-Programme anzuwenden.

Ich bin weiterhin unter biallas[at]embedded[dot]rwth-aachen[dot]de erreichbar.