VU Software Model Checking

Prüfungsinformationen

Es wird von den Studenten erwartet, sich auf die Vorlesung vorzubereiten und die relevanten Publikationen zu lesen.

Die Note ergibt sich aus der Note für ein praktisches Projekt, das von den Studenten implementiert wird, und aus der Mitarbeit während der Vorlesung.

Lernaufwand

Beschreibung

Im Rahmen der Vorlesung werden die Studenten den praktischen Umgang mit existierenden Verifikationstools (so wie CBMC) erlernen und einen eigenen Model Checker entwickeln.

Die Vorlesung beschäftigt sich mit der automatischen Verifizierung von Programmen. Der Fokus liegt hierbei auf den algorithmischen Aspekten der Verifikation. Die Vorlesung setzt sich aus zwei Teilen zusammen:

Im ersten Teil behandeln wir die Verifikation von Modellen mit einem endlichen Zustandsraum (z.B. manuell erstellte Abstraktionen, Zustandsdiagramme, Kontrollsoftware in eingebetteten Systemen).

Im zweiten Teil der Vorlesung erweitern wir diese Ansätze, um die Verifikation von parallelen Programmen und Programmen, deren Zustandsraum nicht a priori beschränkt ist, zu ermöglichen.

  • LVA-Nummer: 184.747
  • ECTS: 6.0
  • Stunden: 4

Module

Vortragende

Beispiele

Möchtest du die Beispiele bewerten musst du dich einloggen. Derzeit funktioniert das über Facebook, wir arbeiten an einem Login über TISS! Facebook Login

Alle Beispiele als ZIP Datei
Add files...