Vorlesung "Formale Spezifikation und Verifikation"

INBB02 - V2 c Inf CV InfMSc CVMSc WInfMSc (Wahlpflicht) - KLIPS
INBB02 - U2 c Inf CV InfMSc CVMSc WInfMSc (Wahlpflicht) - KLIPS

Vorlesung im Sommersemester 2009

Prof. Dr. Bernhard Beckert


Aktuelles

08.07.09: Hinweise zur 2. Übungsaufgabe (abzugeben bis 26.07.09).
08.07.09: Die Blockveranstaltung nach Ende der Vorlesungszeit findet am Mittwoch, dem 05.08.09, und am Donnerstag, dem 06.08.09, statt. Der Raum wird noch bekannt gegeben.
08.07.09: Die Folien zu den Vorlesungen am 09.07. stehen auf der Webseite.
08.07.09: Die Folien zu den Vorlesungen am 18.06., 25.06. und 02.07. stehen auf der Webseite.
27.05.09: Die Folien zur Vorlesung am 28.05. stehen auf der Webseite.
16.05.09: Die 1. Übungsaufgabe steht auf der Webseite. Die Lösung ist bis vor der Vorlesung am 28.05.09 abzugeben.
15.05.09: Die Folien zu den Vorlesungen am 07.05. und 14.05. stehen auf der Webseite.
01.05.09: Die Folien zur gestrigen Vorlesung stehen auf der Webseite.
25.04.09: Die Folien zu den ersten beiden Vorlesungen und Informationen zur Installation des KeY-Systems stehen auf der Webseite.
24.04.09: Vorlesung und Übung finden ab sofort beide nacheinander Donnerstags, 16 Uhr c.t. bis 19:30 in Raum K107, statt (das heißt, am Dienstag, dem 28.04., ist keine Vorlesung).
20.04.09: Da sich die Überschneidungen mit anderen Veranstaltungen bisher nicht zufriedenstellend haben auflösen lassen, findet die erste Vorlesung am Dienstag, dem 21.04.09, um 18 Uhr s.t., in Raum G210 statt. Die endgültigen Termine werden dann gemeinsam mit den Hörern festgelegt.
06.04.09: Vorlesung und Übung finden Dienstag und Donnerstag, jeweils 16 Uhr statt. Da es Überschneidungen mit anderen Veranstaltungen gibt, kann sich das ggf. noch ändern.
28.03.09: Für diese Vorlesung besteht keine Beleg- oder Anmeldepflicht.
28.03.09: Webseite angelegt.

Terminplan

Vorlesung und Übung finden Donnerstags, 16:15 - 19:30 Uhr, Raum K107, statt (mit 15min Pause). Ausfallende Veranstaltungen werden als Block zum Ende des Semesters nachgeholt.

Während der Vorlesungszeit

Di 21.04.09: Vorlesung
Do 23.04.09: Vorlesung
Do 30.04.09: Vorlesung und Übung Do 07.05.09: Vorlesung und Übung
Do 14.05.09: Vorlesung und Übung Do 21.05.09: --- (Feiertag)
Do 28.05.09: Vorlesung und Übung Do 04.06.09: --- (Pfingstferien)
Do 11.06.09: --- Do 18.06.09: Vorlesung und Übung
Do 25.06.09: Vorlesung und Übung Do 02.07.09: Vorlesung und Übung
Do 09.07.09: Vorlesung und Übung Do 16.07.09: ---
Do 23.07.09: Aussprache Promotion Klebanov  

Blockveranstaltung nach Ende der Vorlesungszeit

Der Raum wird noch bekannt gegeben.

Mi 05.08.09
Do 06.08.09
10:15 Uhr: Vorlesung/Übung
10:15 Uhr: Vorlesung/Übung
14:00 Uhr: Vorlesung/Übung
14:00 Uhr: Vorlesung/Übung
16:00 Uhr: Vorlesung/Übung
16:00 Uhr: Vorlesung/Übung

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.

Programme zu spezifizieren und zu verifizieren erfordert Übung (ähnlich wie das Programmieren). Darum werden neben dem Vorlesungsteil auch praktische Übungen einen wesentlichen Teil dieser Veranstaltung ausmachen. Dabei kommt unter anderem das KeY Tool zum Einsatz.

Übungsaufgaben

Die Bearbeitung der Übungsaufgaben ist Pflicht. Zur Prüfung wird nur zugelassen, wer 50% der erreichbaren Punkte erzielt hat. Die Aufgaben sind alleine (nicht in Gruppen) zu bearbeiten.

Materialien

Folien und andere Materialien werden hier jeweils nach der Vorlesung/Übung bereitgestellt.

Folien

KeY-System

SPIN

Zielgruppe

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