Praktikum Spezifikation und Verifikation



!!! Beginn: Mi., 8. Mai um 16:00 im S1128 !!!



Zielgruppe und Voraussetzungen

Dieses Praktikum wendet sich in erster Linie an Studierende nach dem Vordiplom, die sich im Bereich Programmentwicklung (Praktische Informatik) vertiefen wollen. Es ist aber ebenso für Vertiefung im Bereich Semantik und Logik (Theoretische Informatik) interessant.

Das Praktikum erfordert als Voraussetzung Grundkenntnisse einer typisierten funktionalen Programmiersprache (etwa ML, oder Gofer) und ein Interesse am Umgang mit formalen Begriffen und Methoden.

Inhalt

Die Korrektheit von zunehmend komplexeren Hard- und Softwaresystemen zu gewährleisten, ist zu einem ernsten Problem geworden, vor allem in sicherheitskritischen Bereichen [1]. Die zentralen Ziele dieses Praktikums sind das praktische Erlernen Konkret werden einige Anwendungsbeispiele behandelt, wobei wir aus Zeitgründen von vielen Details abstrahieren. Vorgesehen sind u.a.:
  1. Codegenerierung für arithmetische Ausdrücke
  2. Arithmetik-Hardware (nicht die des Pentium!)
  3. Ein Cache-Coherence Protokoll
An jedem dieser Beispiele werden spezifische Modellierungs- und auch Beweistechniken geübt. Die Spezifikation erfolgt jeweils in HOL, die Verifikation in Isabelle [2]. In einer das Praktikum begleitenden Vorlesungsreihe werden die Grundlagen zu Isabelle/HOL vermittelt:
HOL
ist, in erster Näherung, die Anreicherung einer polymorphen funktionalen Programmiersprache um logische Konzepte wie Quantoren und Mengen. HOL ist damit eine ideale Sprache zur Entwicklung funktionaler Programme.
Isabelle
ist ein generischer Theorembeweiser. Eine Ausprägung, Isabelle/HOL, unterstützt Spezifikation und Verifikation in HOL. Es werden verschiedenen Beweisverfahren (Termersetzung, Induktion, etc) vorgestellt und ihre Funktion innerhalb des Beweisprozesses erläutert.

Durchführung

In der ersten Hälfte des Semesters findet eine Vorlesung statt, in der die nötigen Isabelle/HOL Kenntnisse vermittelt werden. Außerdem findet eine wöchentliche Besprechung mit der Praktikumsleitung statt.

Die obigen Anwendungsbeispiele werden in der Vorlesung und der wöchentlichen Besprechung vorgestellt und sind dann innerhalb von 3 Wochen in Gruppen zu bearbeiten und anschließend zu präsentieren.

Zur Durchführung stehen am Lehrstuhl eigene Suns und HPs zur Verfügung. Zusätzlich bieten wir zu festen Zeiten Beratung an.

Literatur

1
W. Wayt Gibbs. Software: chronisch mangelhaft. Spectrum der Wissenschaft, Dezember 1994, 56-63.
2
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, Springer LNCS 828, 1994.