Software and Computational System Lab

Forschungsbereiche:

• Formale Verifikation
• Softwaretechnik
• Programmiersprachen

Aktuelles Projekt:

Software-Verifikation (Software Model-Checking)

Je mehr unsere Gesellschaft und unser persönliches Leben von computerbasierten Geräten abhängt, desto wichtiger ist die korrekte Funktionstüchtigkeit der Computer-Programme, die in solchen Geräten laufen: Vom korrekten Funktionieren unserer Handys und Telefonanlagen hängt es ab, ob wir im Notfall effizient Hilfe rufen können; von der Zuverlässigkeit des Bremssystems unseres Autos hängt es ab, ob wir ggf. einen Unfall vermeiden können. In beiden Fällen sind die wesentlichen funktionalen Bausteine in Software realisiert.

Der Lehrstuhl ist einer der drei führenden Entwickler von Verifikationssoftware für C-Programme. Das Werkzeug CPAchecker bekommt als Eingabe ein C-Programm und eine Spezifikation und untersucht mit erschöpfender Genauigkeit, ob die Spezifikation im gegebenen Programm verletzt werden kann, das heißt, ob eine Fehlfunktion möglich ist. Das Projekt leistet wichtige Beiträge zur Steigerung von Effizienz und Effektivität moderner Verifikationstechnologien. Das Projekt wird in Zusammenarbeit mit der Simon Fraser University in Kanada durchgeführt.

Weitere Informationen: www.sosy-lab.org