Es handelt sich um eine (4+2) Veranstaltung. Um das Modul erfolgreich abzuschließen, sind zwei Leistungen zu erbringen:
Es ist heute sehr selten, dass ein Programm, das effizient sein muss, keine Nebenläufigkeit verwendet. Allerdings hat Nebenläufigkeit ein signifikantes Nachteil: Da die Anzahl der möglichen Verhalten (Interleavings usw.) mit der Anzahl von Threads explodiert, sind Fehler schwierig zu finden, und zu reproduzieren. Daher ist es sehr hilfreich, die Korrektheit dieser Programme automatisiert zu checken bzw. verifizieren. Es gibt verschiedene Ansätze, um diesen Zweck zu erreichen. In dieser Vorlesung behandeln wir die klassischen Methoden, die sich auf automatenartige Strukturen basieren (ähnlich zu Concurrency Theory 2011). Insbesondere werden wir wichtige Ergebnisse in Verifikation von Systemen mit unendlichem Zustandsraum behandeln, wie Verifikation von Wohlstrukturierten Transitionssystemen (WSTS), und das Reachability Problem in Petri Netzen (bzw. Vektoradditionssystemen).
Skripte von vorherigen Semestern:
Handschriftliche Notizen der Vorlesung: