Lehrveranstaltung im Sommersemester 2007

Programmverifikation

Hauptstudiumskurs in Theoretischer Informatik

VAK 03-05-H-699.04, Kategorie A, 6 CP, 4 SWS

Die Frage, ob ein Computerprogramm das tut, was es soll, d.h. ob es festgelegte Anforderungen erfüllt, ist von zentraler Bedeutung in der Softwareentwicklung. Dieses sogenannte Korrektheitsproblem wird sogar lebenswichtig, wenn Computer in sicherheitsrelevanten Bereichen wie z.B. bei der Steuerung von Verkehrsmitteln (Flugzeuge, Eisenbahnen, ...) oder in der Medizin eingesetzt werden.

Programmverifikation ist der systematische Nachweis der Korrektheit von Programmen mit formalen Methoden. Der Kurs gibt eine Einführung in die Verifikation von sequentiellen und parallelen Programmen mit der von Hoare entwickelten axiomatischen Methode.

Letzte Vorlesung: Mo, 30.7.2007, 9:00 s.t. - 12:00, OAS 3000

Fachgespräche und mündliche Prüfungen: Termine

Literatur

Krzysztof R. Apt, Ernst-Rüdiger Olderog: Programmverifikation. Sequentielle, parallele und verteilte Programme. Springer-Lehrbuch, 1994. ISBN 3-540-57479-4. (Errata-Liste von E.-R. Olderog.)
Krzysztof R. Apt, Ernst-Rüdiger Olderog: Verification of Sequential and Concurrent Programs. Springer Texts in Computer Science, 2nd ed., 1997. ISBN 0-387-94896-1.

Voraussetzungen

Grundstudium Informatik.

Folien

Folien vom 07.05.2007 : Scheinbedingungen und Einführung
Folien vom 14.05.2007
Folien vom 21.05.2007
Folien vom 04.06.2007 (Gibt es auch als ps.)
Folien vom 11.06.2007 und Bilder zum Spiel
Folien vom 18.06.2007
Folien vom 25.06.2007
Folien vom 02.07.2007 und noch mehr Bilder zum Spiel, diesmal als .zip
Folien vom 08.07.2007
Ein Beweis in PP

Übungsblätter

Übungsblatt 1
Übungsblatt 2
Übungsblatt 3
Übungsblatt 4, Abgabe bis 21.6.2007, 8:20 Uhr.
Übungsblatt 5
Übungsblatt 6
Übungsblatt 7
Übungsblatt 8

Online-Anmeldung
Kommt demnächst.

Lehrveranstaltende

Prof. Dr. Renate Klempien-Hinrichs	Dipl.-Inf. Caro von Totth
Raum: OAS 3007	Raum: OAS 3006
Telefon: 218-8791	Telefon: 218-8792
kh@biba...	caro@informatik...

Zeit und Raum

Mo 8:00 - 10:00	MZH 7250	Beginn am 7.5.2007
Mo 10:00 - 12:00	MZH 7210

Letzte Vorlesung: Mo, 30.7.2007, 9:00 s.t. - 12:00, OAS 3000

Internes