Beweisbar korrekte Software SS 2007

Vorkenntnis für die Lehrveranstaltung:

Interesse an Logik und formalen Methoden, Vordiplomsveranstaltungen (insb. Logik für Informatiker)

Literatur zur Lehrveranstaltung:

Es besteht eigentlich keine Notwendigkeit, zusätzliche Literatur heranzuziehen. Wer sich dennoch etwas schlauer machen will, kann folgende Bücher heranziehen:

• V. Sperschneider and G. Antoniou, Logic: A Foundation for Computer Science, Addison Wesley, 1991
• J. Loeckx and H.D. Ehrich and M. Wolf, Specification of Abstract Data Types, Wiley-Teubner, 1996

Der Lehrstuhl Softwaretechnik und Programmiersprachen bietet im SS 2007 die Veranstaltung "Beweisbar korrekte Software" (integrierte V + Ü) an.

Die Verwendung formaler Methoden bei der Entwicklung korrekter Software steht an der Schwelle der kommerziellen Nutzung.
Das KIV-System ist ein Werkzeug, das die formale Spezifikation, Verifikation und Synthese von Programmen ermöglicht. Es wird seit mehreren Jahren entwickelt und inzwischen in industriellen Studien erprobt. Übergeordnetes Ziel ist die Produktion beweisbar korrekter Software.

Im Praktikum werden verschiedene klassische Methoden für das Programmieren im Kleinen behandelt. Darüber hinaus kommen innovative Techniken für das Programmieren im Großen zum Einsatz: Spezifikationstechniken und Methoden zum Nachweis der Korrektheit von Moduln und großer, modular strukturierter Systeme.
Das Praktikum vermittelt damit den ''state of the Art'' des Einsatzes formaler Methoden bei der Softwareentwicklung.

Site-Updates & News:

• Die Anmeldung zum Praktikum erfolgt in der ersten Vorlesungsstunde durch Eintragung in eine Liste. Wir können ca. 40 Studenten betreuen. Bei zu vielen entscheidet notfalls das Los.

Scheinerwerb: Erfolgreiche Teilnahme an den Übungen, zwei Abnahmen

Sonstige Informationen: Der praktische Anteil, also das betreute Arbeiten am Rechner, überwiegt. Die Aufgaben müssen auf Papier vorbereitet werden und dann am Rechner gelöst werden.

Abnahme: Die Abnahmen der Aufgaben 4 mit 6 findeen am 16./17.7. statt. Bitte stellt fest, wann Ihr an den beiden Tagen eine Stunde Zeit habt, und kommt dann vorbei (Gruppe 1-10 bei Jonathan, Gruppe 11-20 bei Gerhard), um den Termin abzustimmen. Entsprechend ist die ASM Abgabe schon am 13.7.!

Abgaben im Folgenden:

Logik	3.5.07
Listen	17.5.07
Spezifikation	31.5.07
Hoare Kalkül	14.6.07
Moduln	5.7.07
ASM Refinement	13.7.07

Abgabe jeweils bis 23:59 durch kopieren in das jeweilige home Verzeichnis im Raum 1006

weitere Informationen zu der Lehrveranstaltung:

empfohlenes Studiensemester der Lehrveranstaltung:	Hauptstudium
Fachrichtung Lehrveranstaltung:	Informatik (Dipl., Bachelor, Master)
Nummer der Lehrveranstaltung:	0
Dauer der Lehrveranstaltung:	6 SWS
Typ der Lehrveranstaltung:	WV - Wahlvorlesung
Leistungspunkte:	8 LP für Vorlesung und Praktikum
Bereich:	Softwaretechnik, Theoretische Informatik
Prüfung:	Sonstige
Lehrveranstaltungspflicht:	Wahlpflicht
Semester:	SS 2007