Kurs Grundlagen der Verifikation

Sarah Sallinger MSc

Fehlerfreie Programme zu schreiben ist schwierig. Da Computersysteme immer komplexer werden, ist es selbst mit gründlichem Testen schwierig, knifflige Fehler zu entdecken. In einer zunehmend digitalen Gesellschaft ist die Sicherheit von Computersystemen jedoch von entscheidender Bedeutung, und die Auswirkungen von Fehlfunktionen können katastrophal sein. Formale Verifikation begegnet dieser Herausforderung mit Techniken, die automatisiert überprüfen, ob sich ein System wie vorgesehen verhält. Die wichtigsten Schritte im Verifikationsprozess sind die Definition eines formalen Systemmodells, die Beschreibung des gewünschten Verhaltens in einer formalen Spezifikation und schließlich der Nachweis, dass das Modell die Spezifikation erfüllt.

In diesem Kurs werden wir zentrale Konzepte, Ansätze und Herausforderungen des formalen Verifikationsprozesses kennenlernen. Wir werden anhand praktischer Übungen lernen, wie man einfache Programme modelliert und ihre Korrektheit in einem Model-Checking-Tool verifiziert. Für den praktischen Teil müssen Teilnehmerinnen ihren eigenen Laptop mitbringen.Maximale Teilnehmerinnenzahl: 12 Personen