Praktikum Spezifikation und Verifikation

Prof. Tobias Nipkow, Ph.D.,
Cornelia Pusch

Zeit: Mittwochs 16:20- 18:00
Ort: S1128
Beginn: 6.5.98
Anmeldung: Bei der zentralen Praktikumsanmeldung am Semesteranfang

Das Praktikum zählt sowohl zum Bereich Theorietische wie auch Praktische Informatik.

Voraussetzungen
Motivation und Inhalt
Durchführung
Unterlagen zu den Vorlesungen und Aufgaben
Weitere Informationen
Literatur

Voraussetzungen:

Wir suchen Studierende mit Grundkenntnissen in

   und Interesse an

So solltet Ihr z.B. ohne Probleme ein rekursives funktionales Programm schreiben können, das die ersten n natürlichen Zahlen aufsummiert. Der Begriff der vollständigen Induktion sollte für Euch kein Fremdwort sein, und der Beweis, daß der von obigem Algorithmus berechnete Wert gleich n*(n+1)/2 ist, sollte Euch keine größeren Schwierigkeiten bereiten.


Motivation und 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. Implementierung von Bäumen als Array's.
  2. Arithmetik-Hardware (nicht die des Pentium!) .
  3. Hoare-Logik.
  4. Effiziente Datenstrukturen

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 speziell 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. Hier ist eine Bibliothek existierender HOL Theorien. Im Praktikum werden verschiedene Beweisverfahren (Termersetzung, Induktion, etc.) vorgestellt und ihre Funktion innerhalb des Beweisprozesses erläutert.

A Generic Theorem Prover


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. Die zugehörigen Aufgaben sind dann innerhalb von 1-3 Wochen 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. Weitere Informationen gibt es auf den Merkblättern.

PSV-Mailingliste


Unterlagen zu den Vorlesungen und Aufgaben

1. Vorlesung (6.5.98)

2. Vorlesung (13.5.98)

3. Vorlesung (20.5.98)

4. Vorlesung (27.5.98)

5. Vorlesung (10.6.98)

6. Vorlesung (17.6.98)

7. Vorlesung (24.6.98)

Letzte Aufgabe


Weitere Informationen, Dokumentation etc.

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.
  3. Lawrence C. Paulson. ML for the working programmer, Cambridge University Press,1991.
  4. Daniel J. Velleman. HOW TO PROVE IT: A Structural Approach, Cambridge University Press, 1996.

Zurück zum Anfang


Cornelia Pusch, 27-04-1998