Nebenläufigkeitstheorie SS26

News

16. Februar  - Die Informationen auf dieser Seite sind noch vorläufig.

Organisation

• Der Modulverantwortliche ist Prof. Dr. Roland Meyer. Die Veranstaltung wird zudem von Eren Keskin und Jan Grünke betreut.
• Vorlesung: Dienstag 15:00-16:30 Uhr + Mittwoch 13:15-14:45 Uhr (IZ 358).
• Übung: Donnerstag 15:00-16:30 Uhr (IZ 358).
• Falls Sie die Vorlesung in den Bachelor einbringen möchten, klären Sie dies bitte mit dem Prüfungsamt ab.
• Die Vorlesung beginnt am 14.04.

Modul

Es handelt sich um eine (4+2) Veranstaltung. Um das Modul erfolgreich abzuschließen, sind zwei Leistungen zu erbringen:

• Prüfungsleistung: Zu erbringen durch Bestehen einer mündlichen Abschlussprüfung zu Beginn des vorlesungsfreien Zeitraums. Das genaue Prüfungsdatum wird zeitnah bekannt gegeben.
• Studienleistung: Zu erbringen durch das erfolgreiche Bearbeiten von mindestens 50% der Übungsaufgaben.

Thema

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).

Vorlesungsnotizen

Handschriftliche Notizen der Vorlesung:

• Woche 1: