Beweisbar korrekte Software SS 2008

Downloads:

• Vorlesungsfolien
• Praktikumsdokumentation und -aufgaben

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 2008 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.

Die zweite Abnahme findet am 16. und 17. Juli statt

Verteilung der Übungsgruppen auf die Übungstermine:

Nummer auf der Anmeldung	Gruppennummer	Termine
1	11	14.00/15.45
2	1	10.00/11.45
4	2	10.00/11.45
6	3	10.00/11.45
7	12	14.00/15.45
9	13	14.00/15.45
101	4	10.00/11.45
102	16	14.00/15.45
103	17	14.00/15.45
104	18	14.00/15.45
105	19	14.00/15.45
106	5	10.00/11.45
201	14	14.00/15.45
203	10	11.45/14.00
204	6	10.00/11.45
205	9	10.00/15.45
206	7	10.00/11.45
207	8	10.00/11.45
208	15	14.00/15.45
	20	10.00/11.45

Vorlesungsfolien:

Die Vorlesungsfolien stehen nach jeder Vorlesung zum download bereit.

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.

Abgaben der restlichen Versuche:

Spezifikation	6.6.08
Hoare Kalkül	13.6.08
Moduln	2.7.08
PPL Versuch	14.7.08

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 2008