Semantik und Verifikation paralleler Systeme
Die Arbeitsgruppe Semantik und Verifikation paralleler Systeme wurde Anfang 2019 gegründet und wurde bis Anfang 2023 bis zum Wechsel von Prof. Dr. Marie-Christine Jakobs an die LMU München von ihr geleitet.
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.