Formale Spezifikation und Verifikation

• Material
• Übungsblätter
• Prüfungen
  • Klausur

Aktuelles

• Klausurtermine

  Die Hauptklausur im Sommersemester 2020 findet als Präsenzklausur statt. Termin ist der 05.08.2020, 14-16 Uhr, in den Räumen der Universität.

  Die Vorlesung wechselt mit dem kommenden Semester ins Wintersemester (wieder bei Prof. Ernst) mit einer regulären Prüfung im Februar 2021. Daher können wir auch leider keine Klausur im September/Oktober 2020 anbieten.

  Zuletzt verändert: Do 09 Jul 2020 16:00

• Online Vorlesungs-/Übungsbetrieb

  Da derzeit keine Präsenzveranstaltungen stattfinden können, wir die Vorlesung als wöchentliche Videoaufzeichnung bereitgestellt.

  Bitte entnehmen Sie die Details zur Organisation der Vorlesung dem bereitgestellten Material.

  Zuletzt verändert: So 19 Apr 2020 19:53

Beschreibung

Inhalt

Die Veranstaltung führt in grundlegende Methoden und Konzepte ein, die bei der Spezifikation und Verifikation von Systemen von Bedeutung sind. Es werden Spezifikationsformalismen, Konzepte der System-Modellierung und Grundtechniken für die Automatisierung der Verifikation behandelt. Neben der Vorlesung werden die besprochenen Inhalte im Übungsteil anhand von praktischen Anwendungen eingeübt.
Modulhandbuch, 2.18 P 18: Formale Spezifikation und Verifikation (INF-FSV), Seite 48.

Hörerkreis

Bachelor Informatik

Organisatorisches

Als zentrale Plattform wird Moodle verwendet: https://moodle.lmu.de/course/view.php?id=8545 (Einschreibeschlüssel: FSV). Melden Sie sich dort auf jeden Fall zusätzlich an, bleiben Sie bitte aber auch im Uni2Work Kurs.

Die Vorlesungsfolien sowie Links zu den Aufzeichnungen werden Sie voraussichtlich auf beiden Plattformen finden können.

Ablauf (ab kommender Woche)
- Montag: Veröffentlichung des neuen Vorlesungsmaterials + Übungsaufgaben, Musterlösungen für vorige Woche
- Dienstag: Sprechstunde im Moodle-Chat (ab 12 und ab 14 Uhr)
- Unter der Woche; Betreuung des Forums
- Sonntag: Abgabe der Lösungen, Sie erhalten anschließend eine Korrektur

Manche Übungen werden als zweiwöchentliche Praxisprojekte realisiert, in denen Sie Bonuspunkte für die Klausur erwerben können.
Zur Selbstständigen Lernkontrolle werden wir im Moodle außerdem wöchentlich ein Quiz anbieten.

Weitere Details entnehmen Sie bitte den Organisationsfolien, die wir zeitnah im Uni2Work veröffentlichen werden. Fall Sie Fragen haben, stellen Sie diese bitte im Moodle Forum, gerne dürfen Sie sich auch mit persönlichen Anliegen direkt an uns wenden.

Da die Situation für uns alle neu ist, bitten wir Sie um Nachsicht, falls es mal nicht alles ganz perfekt klappt. Falls Sie Anregungen haben können Sie diese uns gerne zukommen lassen.

Empfohlene Vorkenntnisse

• Logik und Diskrete Strukturen
• Formale Sprachen und Komplexität
• System- oder Softwareentwicklungspraktikum

Links zu allen Video-Aufzeichnungen

20. April

• Organisatorisches
• Motivation
• Einführung und Beispiele

27. April

• Testen: Überblick
• Unit-Testen

4. Mai

• Property-based Testing
• Kontrollflussautomaten und Abdeckungsmaße

11. Mai

• Transitionssysteme
• Explizite Erreichbarkeitsanalyse

19. Mai

• Nichtdeterminismus
• Symbolische Erreichbarkeitsanalyse

29. Mai

• Wiederholung & Schleifeninvarianten
• Einführung in Dafny

10. Juni

• Floyd/Hoare Logik

15. Juni

• Tutorium: Testen, Erreichbarkeitsanalysen, Hoare-Logik

25. Juni

• Hoare Logik: Prozeduren
• Klassen: Spezifikation
• Klassen: Verifikation
• Dafny: ArrayList

30. Juni

• SAT/SMT

Literatur

• Edmund M. Clarke, Orna Grumberg, and Doron Peled: Model Checking. MIT Press, 2000.
• Gerard J. Holzmann: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.
• Zohar Manna and Amir Pnueli: Temporal verification of reactive systems: Safety. Springer,1995.
• Flemming Nielson, Hanne Riis Nielson, and Chris Hankin: Principles of Program Analysis. Springer, 2004.
• Christel Baier and Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.

Institut

Institut für Informatik

Dozent:in

• Gidon Ernst

Assistent:innen

• Stephan Holzner
• Martin Spießl

Korrektor:innen

• Philipp Althaus
• Stephan Holzner
• Sudeep Kanav
• Martin Spießl

Kursteilnehmer:innen

311

Anmeldung

So 01 Mär 2020 00:00 – Mi 30 Sep 2020 23:59

Abmeldung nur bis Mi 30 Sep 2020 23:59

Material

Die Übungsblatter zum Kurs finden Sie hier: Übungsblätter

Material zum Kurs finden Sie hier: Material

Das Kursmaterial ist ohne Anmeldung frei zugänglich

Prüfungen

Name	Anmeldung ab	Anmeldung bis	Termin	Prüfungsanmeldung
Klausur	Di 07 Jul 2020 12:00	Do 30 Jul 2020 23:55	Mi 05 Aug 2020 14:00 – 16:00	Nicht zur Prüfung angemeldet

Tutorien

Art	Bezeichnung	Tutoren	Regulärer Raum	Zeit	Anmeldungen ab	Anmeldungen bis	Abmeldungen bis	Freie Plätze
Klausureinsicht	Klausureinsicht Block 1		U151, Oettingenstrasse 67	Di 10:00–11:00 Findet statt: Di 06 Okt 2020 10:00–10:30	Mi 30 Sep 2020 00:00	Di 06 Okt 2020 00:00	Di 06 Okt 2020 00:00	22
Klausureinsicht	Klausureinsicht Block 2		U151, Oettingenstrasse 67	Di 06 Okt 2020 10:30–11:00	Mi 30 Sep 2020 00:00	Di 06 Okt 2020 00:00	Di 06 Okt 2020 00:00	20
Klausureinsicht	Klausureinsicht Block 3		U151, Oettingenstrasse 67	Di 06 Okt 2020 11:00–11:30	Mi 30 Sep 2020 00:00	Di 06 Okt 2020 00:00	Di 06 Okt 2020 00:00	22
Klausureinsicht	Klausureinsicht Block 4		U151, Oettingenstrasse 67	Di 06 Okt 2020 11:30–12:00	Mi 30 Sep 2020 00:00	Di 06 Okt 2020 00:00	Di 06 Okt 2020 00:00	18