Am Institut für Formale Modelle und Verifikation (FMV), geleitet von Prof. Bernhard Aichernig, beschäftigen wir uns mit der Forschung und praktischen Anwendung formaler Methoden in der Softwareentwicklung. Formale Methoden sind mathematisch präzise Techniken und Werkzeuge, mit denen Software- und Hardwaresysteme spezifiziert, entworfen und verifiziert werden können.

Unsere Arbeit deckt alle Phasen der Entwicklung ab — von der Anforderungserhebung über Testen und Verifikation bis hin zum Reverse Engineering. Unser Ziel ist es, sicherzustellen, dass Systeme unter allen denkbaren Bedingungen korrekt funktionieren. Aktuell erweitern wir unsere Forschung auch auf die Zuverlässigkeit von KI-Systemen.

Unsere Forschungsfelder im Überblick:
    • Spezifikation & Entwurf beschäftigt sich mit den frühen Phasen der Entwicklung. Dabei geht es darum, passende Abstraktionen und formale Modelle für komplexe Probleme zu finden.
    • Automatenlernen entwickelt Methoden und Tools, um automatisch formale Modelle aus vorhandenen Daten (passives Lernen) oder durch gezielte Tests eines Systems (aktives Lernen) zu erzeugen. So lassen sich Systeme auch dann analysieren, wenn man keinen Zugriff auf deren Interna hat.
    • Falsifikation konzentriert sich auf das Testen von Software. Hier erforschen wir unter anderem Verfahren zur automatischen Testfall-Generierung, um Schwächen und Fehler schnell und effizient aufzudecken.
    • Verifikation hat das Ziel, zu beweisen, dass ein Software-System oder eine Komponente fehlerfrei ist. Mit Techniken wie der beweisbasierten Entwicklung entsteht Software, die von Anfang an korrekt ist.

Unser Team verbindet eine starke theoretische Basis in formalen Methoden mit der praktischen Anwendung in unterschiedlichen Industriezweigen — unter anderem auch in der Automobilbranche.