Suche

06233


Physik Wintersemester 2002/2003
06233 Beweisbar korrekte Software Praktikum [WV]
   
Dozent Reif, Stenzel, Duelli
Dauer 2 SWS
Studiensemester 5
Schein Ja
Termin Di, 12:30-14:00, 1006/NW I
Beginn 14.10.2002
Inhalt 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.

Begleitend 06234
Vorkenntnisse Interesse an Logik und formalen Methoden.
Literatur Praktikumsunterlagen werden zu Beginn des Praktikums ausgegeben.
Weitere Informationen Ablauf: Vorbereitung der Aufgaben auf Papier (zuhause), dann betreutes Arbeiten am Rechner.