Vorlesung "Grundlagen der Programmsicherheit" (SS 10)

Prof. Dr. M. Lange

---

Inhaltsverzeichnis dieser Seite

Aktuelles

• 7.9.10, 14:00 Uhr: Die Termine für die mündlichen Prüfungen können nun vergeben werden. Es sind zunächst mehrere Termine am Montag/Dienstag, 27. und 28.9. vorgesehen - siehe auch die Tabelle weiter unten. Die Prüfungen finden im Raum 1318 (FG Formale Methoden und Verifikation) statt. Um einen Termin zu bekommen, schickt bitte eine Email mit einem Vorschlag für einen noch nicht belegten Slot an "martin dot lange at uni minus kassel dot de".

Organisatorisches

Umfang: 4 SWS

Zeit und Ort: Mo 12-14, Do 8-10, WA -1319

Dozent: Prof. Dr. Martin Lange

Vorkenntnisse:

Theoretische Informatik: Berechenbarkeit und formale Sprachen

Theoretische Informatik: Logik

Algorithmen und Datenstrukturen

Hörerkreis:

Studierende der Informatik im Hauptstudium

Studierende mit Nebenfach Informatik

Prüfungen

Termin	Kandidat
Montag, 27.9., 10:00 Uhr	Tausendfreund
Montag, 27.9., 10:30 Uhr	Herwig
Dienstag, 28.9., 10:00 Uhr	Durhack
Dienstag, 28.9., 10:30 Uhr	Opfer
Dienstag, 28.9., 13:30 Uhr	Iffländer
Dienstag, 28.9., 14:00 Uhr	George
Dienstag, 28.9., 14:30 Uhr	Glogic

Zeitplan:

Tag	Datum	Veranstaltung
Mo	12.04.	Vorlesung
Do	15.04.	Vorlesung
Mo	19.04.	Vorlesung
Do	22.04.	Vorlesung
Mo	26.04.	Vorlesung
Do	29.04.	Übung
Mo	03.05.	Vorlesung
Do	06.05.	Vorlesung
Mo	10.05.	Übung
Do	13.05.	(Christi Himmelfahrt)
Mo	17.05.	Vorlesung
Do	20.05.	Vorlesung
Mo	24.05.	(Pfingstmontag)
Do	27.05.	Übung
Mo	31.05.	Vorlesung
Do	03.06.	(Fronleichnam)
Mo	07.06.	Vorlesung
Do	10.06.	Übung
Mo	14.06.	Vorlesung
Di	15.06., 18-20, -1605	Vorlesung
Do	17.06.	Übung
Mo	21.06.	Vorlesung
Di	22.06., 18-20, -1605	Vorlesung
Do	24.06.	Übung
Mo	28.06.	Vorlesung
Do	01.07.	Vorlesung
Mo	05.07.	Übung
Do	08.07.	(fällt aus)
Mo	12.07.	(fällt aus)
Do	15.07.	(fällt aus)

Sondertermine nach Absprache in den ersten Vorlesungen.

---

Inhalt

• Verifikation: Motivation, fehlerbehaftete Systeme, Programme und Modelle, Verifikationstechniken, Model Checking
• Modellierung: Transitionssysteme, Semantik, Abstraktion, Läufe, Äquivalenzbegriff
• Linearzeit-Eigenschaften: Invarianten, Safety, Liveness, Fairness
• Automaten auf unendlichen Wörtern: Büchi-Automate, Verifikation ω-regulärer Eigenschaften, generalisierte Büchi-Automaten
• Linearzeit-Temporallogik: LTL, LTL und Büchi-Automaten
• Baumzeit-Temporallogik: CTL, Model Checking, symbolisches Model Checking, BDDs

---

Material

Vorlesungsfolien:

Tageweise (mit Overlays):

• Folien vom 12.04. als PDF
• Folien vom 15.04. als PDF
• Folien vom 19.04. als PDF
• Folien vom 22.04. als PDF
• Folien vom 26.04. als PDF
• Folien vom 03.05. als PDF
• Folien vom 06.05. als PDF
• Folien vom 17.05. als PDF
• Folien vom 20.05. als PDF
• Folien vom 31.05. als PDF
• Folien vom 07.06. als PDF
• Folien vom 14.06. und 15.6. als PDF
• Folien vom 21.06. als PDF
• Folien vom 22.06. als PDF
• Folien vom 28.06. als PDF
• Folien vom 01.07. als PDF

Kapitelweise (ohne Overlays):

• Kapitel 0: Überblick
• Kapitel 1: Einführung in die formale Verifikation
• Kapitel 2: Modellierung nebenläufiger und reaktiver Systeme
• Kapitel 3: Linearzeit-Eigenschaften
• Kapitel 4: Automaten auf unendlichen Wörtern
• Kapitel 5: Linearzeit-Temporallogik
• Kapitel 6: Baumzeit-Temporallogik

Übungsblätter:

• Blatt 1 (PDF) vom 22.04.10, Bearbeitung bis zum 29.4.10
• Blatt 2 (PDF) vom 03.05.10, Bearbeitung bis zum 10.5.10, mit Lösung eines Teils von Aufgabe 7
• Blatt 3 (PDF) vom 20.05.10, Bearbeitung bis zum 27.5.10
• Blatt 4 (PDF) vom 04.06.10, Bearbeitung bis zum 10.6.10
• Blatt 5 (PDF) vom 10.06.10, Bearbeitung bis zum 17.6.10
• Blatt 6 (PDF) vom 17.06.10, Bearbeitung bis zum 24.6.10
• Blatt 7 (PDF) vom 24.06.10, Bearbeitung bis zum 5.7.10

Literatur:

• Ch. Baier, J.-P. Katoen, Principles of Model Checking, MIT Press, 2008

---

Links

• Verifikationstools:
  • Spin