TU München  Informatik  Software & Systems Engineering  Theorem Proving Group  Lehre

Isabelle Praktikum Spezifikation und Verifikation

Prof. Tobias Nipkow
Martin Strecker

Fragen Sie sich auch immer wieder, ob Ihr Programm wirklich funktioniert?
Wollten Sie schon immer verstehen, was Ihr Programm eigentlich macht?

Dann sind Sie hier richtig!

 

Zeit:
Mittwochs 16:00 - 18:00
Ort:
00.11.038 (Raum John v. Neumann)
Beginn:
22.10.2003
Aktuell:
Am 26.11.2003 findet keine Vorlesung statt!!
Anmeldung:
Alle verfügbaren Plätze sind bereits belegt.
Zuordnung:
Das Praktikum zählt zum Bereich Theoretische Informatik.

 

Voraussetzungen

Wir suchen Studierende mit Grundkenntnissen in und Interesse an

So sollten Sie z.B. ein rekursives funktionales Programm schreiben können, das die natürlichen Zahlen 1, ..., n aufsummiert. Der Begriff der vollständigen Induktion sollte kein Fremdwort sein, und der Beweis, daß der von obigem Algorithmus berechnete Wert gleich n(n+1)/2 ist, keine fundamentalen Schwierigkeiten bereiten.

Motivation und Inhalt

Die Korrektheit von sicherheitskritischen Hard- und Softwaresystemen zu gewährleisten, ist immer noch ein ernstes Problem. Die zentralen Ziele dieses Praktikums sind das Erlernen

Konkret werden einige Anwendungsbeispiele behandelt, wobei wir aus Zeitgründen von vielen Details abstrahieren. Vorgesehen sind u.a.

An jedem dieser Beispiele werden spezifische Modellierungs- und Beweistechniken geübt. Die Spezifikation und Verifikation erfolgt in Isabelle/HOL.

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 Beschreibung funktionaler Programme.
Isabelle
ist ein generischer Theorembeweiser. Eine Ausprägung, Isabelle/HOL, unterstützt Spezifikation und Verifikation in HOL. Im Praktikum werden verschiedene 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. Die Aufgaben sind jeweils innerhalb von 1-3 Wochen zu bearbeiten und bei der Praktikumsleitung zu präsentieren (Termin nach Vereinbarung). Die Bearbeitung erfolgt in Gruppen von je 2 Personen.

Als Arbeitsumgebung stehen die sunhalle-Rechner und die am Lehrstuhl üblichen Sparc/Solaris und x86/Linux Plattformen zur Verfügung.

Mario Ullrich, Joachim Biggel Stefan Berghofer
Christian Knörndel, Christian Ehmig Farhad Mehta
Tao Yu, Yajie Wang Steven Obua
René Frieß, Benedikt Elser Norbert Schirmer
Chuan Tao, Qinzhao Cheng Sebastian Skalberg
Alexander Ludwig, Thomas Morandell Martin Strecker
Christina Kuhn, Claudia Milew, Sylvia Wowerat Martin Strecker
Liming Lin, Matthias Nöbl, Werner Jansen Tjark Weber
Zhen Zhang, Yuxiang Liang Martin Wildmoser

Arbeitsunterlagen und Aufgaben

Dokumentation

Vorlesungsunterlagen

Aufgaben

Aktuelle Hinweise

(1) Rechnerbenutzung

Sie erhalten von der Praktikumsleitung eine Kennung auf den Unix Systemen des Lehrstuhls Broy (Link funktioniert nur von den Lehrstuhlrechnern aus). Der entsprechenden Rechnerraum ist 01.11.034.

(2) Starten von Isabelle

Auf den sunbroy und sunhalle Rechnern läßt sich Isabelle (zusammen mit der Proof General Benutzeroberfläche) wie folgt starten: 

        /usr/proj/isabelle/bin/Isabelle

Mit 

        /usr/proj/isabelle/bin/isatool install -p ~/bin
kann man sich das Isabelle binary auch im eigenen ~/bin Verzeichnis installieren.

Unter KDE lässt sich ein Application Desktop-Objekt zum Anklicken erzeugen: 

        /usr/proj/isabelle/bin/isatool install -k

Für zügiges Arbeiten mit Isabelle sollte man eine relativ robuste Maschine verwenden, am Lehrstuhl etwa die sunbroy60, sunbroy61, sunbroy1, oder einen sunhalle Rechner.

(3) Isabelle zuhause installieren

Sie können Isabelle recht einfach auf dem eigenen PC zuhause installieren. Isabelle sollte gut mit allen gängigen Linux-Distributionen zusammenarbeiten. Angenehmes Arbeiten ist ab ca. 128M Arbeitsspeicher und einer 500Mhz CPU möglich.

Weitere Hinweise zur Installation und eine vorkompilierte Isabelle-Version finden sie auf unserer download Seite.

(4) Hinweise für die abschließende Präsentation

Zum Abschluß des Praktikums findet eine Präsentation der letzten Aufgabe in Form eines 20- bis 25-minütigen Vortrags statt, an dem alle Teilnehmer einer Gruppe beteiligt sein sollten. Die Präsentation findet in Raum 00.11.038 statt.

Für den Vortrag steht Ihnen ein Beamer und Notebook zur Verfügung, Sie können aber auch einen Tageslichtprojektor verwenden.

Literatur

  1. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel Isabelle/HOL - The Tutorial, TU München, 2001.
  2. Markus Wenzel. The Isabelle/Isar Reference Manual, TU München, 2002. (mehr über Isar)
  3. Lawrence C. Paulson. ML for the working programmer, Cambridge University Press, 1996.
  4. Daniel J. Velleman. How to Prove it: A Structural Approach, Cambridge University Press, 1996.

 
Martin Strecker Last modified: Fri Mar 26 09:55:52 MET 2004