Programmiersprachen und Tools Lab

Model Checking Concurrent Programs

Im Rahmen dieses Projekts arbeiten wir an Modellprüfungstools, die dabei helfen, komplexe Fehler in nebenläufigen Programmen zu entdecken.

Es ist schwierig, nebenläufige Algorithmen korrekt zu schreiben. Übliche Testverfahren sind im Zusammenhang mit nebenläufigen Programmen nicht sehr hilfreich, da sich diese Programme nicht deterministisch verhalten und einige Fehler nur in einer bestimmten Umgebung auftreten können (z. B. im entspannten Speichermodell einer bestimmten Hardware).

Model Checking ist eine formale Verifikationsmethode, die dabei hilft, Fehler in nebenläufigen Programmen aufzudecken, indem verschiedene Ausführungsspuren eines Programms in einer kontrollierten Umgebung systematisch untersucht werden.

In diesem Projekt entwickeln wir neue Methoden, um dieses Problem anzugehen, und versuchen, bestehende Model-Checking-Tools für nebenläufige Programme zu verbessern und sie in realen Softwareprojekten zu testen.

Teilnehmende

Evgenii Moiseenko