Semantik und Verifikation paralleler Systeme

Mitarbeiter/in gesucht

Zur Verstärkung der Arbeitsgruppe suchen wir aktuell eine(n) neue(n) wiss. Mitarbeiter/in. Details entnehmen Sie bitte dem Ausschreibungstext.

Arbeitsgruppe Semantik und Verifikation paralleler Systeme

Die Arbeitsgruppe Semantik und Verifikation paralleler Systeme wurde Anfang 2019 gegründet und wird von Prof. Dr. Marie-Christine Jakobs geleitet.

Unser Forschungsgebiet

Softwareverifikation beschäftigt sich mit der Fragestellung, ob ein Programm gewisse Eigenschaften erfüllt. Eigenschaften von Interesse sind vielfältig. Zum Beispiel kann man sich für Laufzeitfehler wie Division durch Null oder Dereferenzierung eines Nullzeigers interessieren, die Terminierung von Programmen untersuchen oder die Funktion eines Programms prüfen, also zum Beispiel prüfen, ob ein Programm eine gegebene Liste sortiert.

Softwareverifikation ist von großer Bedeutung für unsere aktuelle Gesellschaft. Softwaresysteme finden sich in immer mehr Lebensbereichen. Während ein Absturz unseres Smartphones aufgrund eines Softwarefehlers lediglich ärgerlich ist, kann ein Softwarefehler in sicherheitskritischen Systemen wie zum Beispiel autonomen Fahrzeugen katastrophale Folgen haben.

Damit Eigenschaften eines Programms geprüft werden können, muss die Semantik eines Programms bekannt sein. Die Semantik des Programms beschreibt auf welche Art und Weise das Programm von einem Computer ausgeführt werden kann.

Unser Forschungsschwerpunkt

Wir nutzen formale Methoden zur Softwareverifikation, das heißt unsere Ansätze basieren auf mathematischen Grundlagen. Im Bereich der formalen Methoden setzen wir vor allem auf statische Programmanalyse und Model Checking. Unser Fokus liegt auf der Verifikation von Eigenschaften paralleler Softwaresysteme. Wir beschränken uns damit nicht nur auf die theoretische Grundlagenforschung, sondern möchten unsere Ansätze auch gleichermaßen in Verifikationswerkzeugen umsetzen.

Zu unseren aktuellen Forschungsinteressen zählen zum Beispiel die inkrementelle Verifikation, die Kombination von Verifikationsansätzen sowie die Prüfung von Verifikationsergebnissen. Details erfahren Sie auf unseren Forschungswebseiten oder in unseren Publikationen.

Unser Lehrangebot

Zu unserem regelmäßigen Lehrangebot gehören integrierte Veranstaltungen zum Thema Automatische Softwareverifikation und Verifikation paralleler Systeme. Außerdem bieten wir regelmäßig ein Seminar zu aktuellen Themen aus unserem Forschungsgebiet an. Wenn Sie sich für eine Abschlussarbeit bei uns interessieren, informiert Sie unsere aktuelle Themenliste über potentielle Abschlussarbeiten. Auf Anfrage können wir auch gemeinsam mit Ihnen ein Abschlussarbeitsthema konzipieren.

Forschen Sie mit uns

Wenn Sie sich für die Forschung von unserer Arbeitsgruppe interessieren, gibt es verschiedene Möglichkeiten bei uns mitzuarbeiten.

Als Studierende(r) können Sie zum Beispiel Ihre Abschlussarbeit bei uns schreiben. Wir suchen auch regelmäßig studentische Hilfskräfte, die uns bei der Lehre oder Forschung unterstützen. Falls Sie Interessen an einer solchen Tätigkeit haben, nehmen Sie Kontakt mit uns auf.

Wenn Sie sich für eine Promotion in unserer Arbeitsgruppe interessieren, wenden Sie sich bitte an Prof. Dr. Marie-Christine Jakobs.

Wir sind generell interessiert an Kooperationen mit Industriepartnern oder anderen Forschergruppen. Wenn Sie Vorschläge und Ideen für eine Kooperation haben, kontaktieren Sie Prof. Dr. Marie-Christine Jakobs.