Formal Methods for Fun and Profit

Seminar im Sommersemester 2005

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,

• wo und wie schon heute formale Methoden in der Praxis eingesetzt werden,
• welche formalen Methoden in der Praxis erfolgreich sind und warum,
• was die Zukunft für die formalen Methoden verspricht.

Lernziele sind bei diesem, wie bei jedem anderen Seminar:

• Selbständiges Erarbeiten eines vorgegebenen Themas
• Vorbereiten und Halten eines Fachvortrags
• Auseinandersetzung mit und Diskussion über Fachvorträge

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

• Grundlagen der Verifikation: Hoare-Logik
  (Vortragende: Julia Schapring; Betreuer: Bernhard Beckert)
• Grundlagen der Verifikation: Model checking
  Folien -  Ausarbeitung
  (Vortragende: Sabine Bauer; Betreuer: Vladimir Klebanov)
• Spezifikation von Software: JML, SPEC#
  (Vortragende: Nadine Gille; Betreuer: Vladimir Klebanov)
• Spezifikation von Hardware: VHDL
  (Vortragender: Ilja Kipermann; Betreuer: Gerd Beuster)
  Folien -  Ausarbeitung
  
• Kosten und Nutzen formaler Methoden
  (Vortragender: Maik Stange; Betreuer: Bernhard Beckert)
• Formale Methoden und systematisches Testen
  (Vortragender: Rodja Trappe; Betreuer: Bernhard Beckert)
• Formale Methoden: von Theorien zur Ingenieurwissenschaft
  (Vortragender: Emanuel Knoepfel; Betreuer: Gerd Beuster)
• Zertifizierung von Soft- und Hardware
  (Vortragender: Andrew Kiprop; Betreuer: Gerd Beuster)
  Folien -  Ausarbeitung
  
• 30 Jahre Verifikationswerkzeuge: Von Boyer-Moore bis KeY
  Folien -  Ausarbeitung
  (Vortragender: Niklas Henrich; Betreuer: Vladimir Klebanov)
• Das SLAM-Projekt bei Microsoft
  (Vortragende: Anke Schneider; Betreuer: Bernhard Beckert)
• Software-Model-Checking mit Bandera
  (Vortragender: Thorsten Bormer; Betreuer: Vladimir Klebanov)
• Verifikation der Fliesskomma-Arithmetik bei Intel
  (Vortragender: Dennis Willkomm; Betreuer: Gerd Beuster)
  Folien - Ausarbeitung
  

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

• Halten (in freier Rede) eines selbständig und sorgfältig erarbeiteten Vortrags von ca. 45min
• Anwesenheit bei allen Seminarvorträgen und Beteiligung an der Diskussion nach den Vorträgen
• Anfertigung einer Ausarbeitung zum Thema des Vortrags von 10-15 Seiten. Wie bei wissenschaftlichen Konferenzen üblich soll hierfür der LNCS-Style des Springer-Verlags verwendet werden. Formatvorlagen für LaTeX und MS Word können von der Springer-Webseite heruntergeladen werden. Nutzer von MS Word müssen ihre Ausarbeitung als PostScript oder PDF einreichen. Wir empfehlen die Verwendung von LaTeX. Eine Einführung in LaTeX finden sie hier.

LaTeX

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

• LaTeX-Kurzbeschreibung
• Informationen zu prosper

Bernhard Beckert