VU Software Model Checking

Exam informations

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.

Workload for exams

Description

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

Lecturers

Examples

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

Download all as ZIP File
Add files...