Formal Methods for Fun and Profit

4.1.31 S2 c CV c In

Seminar im Sommersemester 2005

Jun.-Prof. Dr. Bernhard Beckert
Gerd Beuster
Vladimir Klebanov

Aktuell

Das Seminar findet im Raum B016 zu folgenden Zeiten statt:
Montag 15.8.: 15-18 Uhr
Dienstag 16.8.: 10-13 und 14-18 Uhr


Allgemeine Informationen

Mit formalen Methoden können Soft- und Hardware-Systeme auf abstrakter Ebene präzise beschrieben werden. Sie erlauben eine exakte Spezifikation der Eigenschaften von Systemen und können Ausgangspunkt einer formalen Verifikation sein, in der formal-logisch bewiesen wird, dass eine Implementierung die Spezifikation erfüllt. Formale Spezifikation ist aufwändiger als umgangssprachliche oder semi-formale Spezifikation. Zudem erfordert der Beweis der Korrektheit eines Systems durch Verifikation besondere Kenntnisse und Werkzeuge und ist aufwändig. In der Praxis konnten sich formale Methoden deshalb bisher kaum durchsetzen. In diesem Seminar soll untersucht werden,

Lernziele sind bei diesem, wie bei jedem anderen Seminar:

Der Besuch der ebenfalls im Sommersemester 2005 angebotenen Vorlesung "Formale Verifikation von Software" (4.1.12 im Vorlesungsverzeichnis) ist eine sinvolle Ergäzung aber keine notwendige Voraussetzung für die Teilnahme am Seminar.


Vortragsthemen


Organisatorisches

Das Seminar findet als Blockveranstaltung an zwei Tagen am Ende der Vorlesungszeit statt (nach Möglichkeit in der ersten vorlesungsfreien Woche, der genaue Termin wird im Einvernehmen mit den Teilnehmern festgelegt). Eine Vorbesprechung findet Anfang des Semester in der ersten Vorlesungswoche statt. Der Termin wird rechtzeitig bekanntgegeben. Bitte melden Sie sich über MeToo für das Seminar an. Wenn sie weitere Fragen haben, schreiben Sie bitte an Bernhard Beckert

Bis Ende Mai soll die Literatur gesichtet sein und eine Gliederung des Vortrags vorliegen. Bis Ende Juni sollen Entwürfe der Folien und der Ausarbeitung vorliegen. Die endgültigen Fassungen der Folien und der Ausarbeitung müssen zwei Wochen vor dem Vortragstermin vorliegen.


Voraussetzungen zur Erlangung des Scheins


LaTeX

Für die Erstellung der Folien sei das prosper-Package empfohlen.


Bernhard Beckert