Vorlesung "Formale Spezifikation und Verifikation"

INBB02 - 4.1.24 V3 c Inf (KITE + ST) CV InfMSc CVMSc - KLIPS
INBB02 - 4.1.25 Ü1 c Inf (KITE + ST) CV InfMSc CVMSc - KLIPS
Summer Academy

Vorlesung im Sommersemester 2008

Prof. Dr. Bernhard Beckert
Christoph Gladisch
cVladimir Klebanov

Aktuelles

26.07.08: Die Materialen zu den Übungen stehen auf der Webseite zur Verfügung.
22.07.08: Die Prüfung zur Vorlesung findet mündlich statt. Termine können individuell vereinbart werden.
22.07.08: Die Folien zum Vorlesungsteil der Blockveranstaltung stehen nun auf der Webseite zur Verfügung.
15.07.08: All the remaining lectures have been moved to room B017.
22.06.08: Die Blockveranstaltung findet in Raum A308 statt, mit Ausnahme der Vorlesung am Mittwoch Morgen, die nach Raum A213 verlegt ist.
22.06.08: Die Materialien zu Model Checking stehen zur Verfügung
22.06.08: Sätliche Termine stehen nun fest (s.u.)
22.06.08: Weitere Materialien stehen zur Verfügung

Termine

Während der Vorlesungszeit findet die Vorlesung zu beiden Terminen
regelmäßig stattfinden. Dabei wird sie aber so häufig ausfallen (Termine werden hier bekannt gegeben), dass dies einer dreistündigen Vorlesung enstpricht. Hier der Terminplan für die Vorlesung:

Dienstag
 Donnerstag
08.04.08: ---
 10.04.08: ---
15.04.08: Vorlesung 17.04.08: Vorlesung
22.04.08: Vorlesung 24.04.08: Vorlesung
29.04.08: Vorlesung 01.05.08: --- (Mai-Feiertag)
06.05.08: Vorlesung 08.05.08: Vorlesung
13.05.08: --- (Pfingstferien) 15.05.08: --- (Pfingstferien)
20.05.08: Vorlesung 22.05.08: --- (Fronleichnam)
27.05.08: --- 29.05.08: Vorlesung
03.06.08: --- 05.06.08: ---
10.06.08: Vorlesung 12.06.08: Vorlesung
17.06.08: Vorlesung 19.06.08: Vorlesung
24.06.08: --- 26.06.08: Vorlesung
01.07.07: --- 03.07.08: Vorlesung
08.07.08: --- 10.07.08: ---
15.07.08
 16.07.08
 17.07.08
10:15 Uhr: Vorlesung (A308)
 10:15 Uhr: Vorlesung (B017)
 10:15 Uhr: Vorlesung (B017)
14:00 Uhr: Übung (A308)
 14:00 Uhr: Übung (B017)
 14:00 Uhr: Übung (B017)
16:00 Uhr: Übung (A308)
 16:00 Uhr: Übung (B017)
 16:00 Uhr: Übung (B017)

Materialien

15.04.08: Introduction - Folien; Quiz
17.04.08: Introduction - Folien; Lösung zum Quiz
22.04.08: Formal Specification - Folien A, Folien B; Beispielprogramme TestAlwaysTrue.java, TestAlwaysTrue2.java, Book-wrong.java, Book-correct.java, AddTwoBooks.java, TestBookEq.java, Library.java
24.04.08: Formal Specification - Folien
24.04.08: Java Modelling Language - Folien
29.04.08: Beispiele zur Java Modelling Language - Question1.java, Queue.java
06.05.08: Object Constraint Language - Folien
08.05.08: Beispiele zur Object Constraint Language - Folien A, Folien B
20. und 29.05.08: Das Tutorial zur Common Algebraic Specification Language: GENTLE.pdf. Weitere Informationen zu CASL gibt es auf der Webseite der CoFI
10., 12. und 17.06.08: Abstract State Machines - Folien
19.06.08: Modallogik - Folien
26.06.08: Model Checking - Folien A, Folien B (diese Vorlesungsfolien wurden M. Dwyer, J. Hatcliff und Robby von der Kansas State University erstellt)
03.07.08: Model Checking - Folien (diese Vorlesungsfolien wurden M. Dwyer, J. Hatcliff und Robby von der Kansas State University erstellt)

Blockveranstaltung (15.-17.07.08): Übungen:

Zielgruppe

Die Vorlesung richtet sich an Studierende der Diplom- und Master-Studiengänge Informatik und CV. Im Master-Studiengang zählt sie zum Schwerpunkt "Data and Knowledge Engineering", im Diplom-Studiengang zu den beiden Vertiefungsbereichen KITE und ST.

Inhalt

Diese Veranstaltung soll die Studierenden in die Lage versetzen, die verschiedenen Techniken der formalen Spezifikation und Verifikation von Software (insbes. objekt-orientierter Software) zu verstehen und praktisch anzuwenden.
Bernhard Beckert