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

Isabelle Praktikum Spezifikation und Verifikation

Prof. Tobias Nipkow
Steven Obua

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:
Mittwoch, 16:00-18:00
Ort:
im Raum Konrad Zuse (01.11.018)
Beginn:
Mittwoch, 26. 4. 2006
Anmeldung:
Die Anmeldung ist abgeschlossen.
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, dass 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 ist u.a. die

Es werden aber auch Grundlagen behandelt wie

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 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 / Gruppeneinteilung

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. Idealerweise finden Sie sich selbst direkt nach der ersten Vorlesung zu Gruppen zusammen und teilen diese dann der Praktikumsleitung mit.

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

Christian Varadi (varadi), Maximilian Wahler (wahlerm) Stefan Berghofer
Zied Tfifha (tfifha), Sebastian Zeller (zellers) Amine Chaieb
Thomas Schneider (schneidt), Christoph Erdle (erdle) Steven Obua
Boris Borisov (borisovb), Georgi Georgiev (georgiev) Tjark Weber
Matthias Häring (matthias.haering bei web.de), Lars Goldammer (lars.goldammer bei mytum.de) Markus Wenzel
Nataliya Starchenko (starchen), Christoph Mair (mair) Norbert Schirmer
Thorsten Keller (kellert), Patrick Schellhorn (schellho) Florian Haftmann
Andreas Schaumeier (schaumei), Kai Römer (roemerk) Alexander Krauss


Präsentationstermine

Die Präsentationen finden im Raum Alan Turing (00.09.055) statt, bitte kommen Sie nur zu IHRER EIGENEN Präsentation.

15:25 Christian Varadi, Maximilian Wahler Stefan Berghofer
16:15 Zied Tfifha, Sebastian Zeller Amine Chaieb
15:50 Thomas Schneider, Christoph Erdle Steven Obua
13:45 Boris Borisov, Georgi Georgiev Tjark Weber
15:00 Matthias Häring, Lars Goldammer Markus Wenzel
14:35 Nataliya Starchenko, Christoph Mair Norbert Schirmer
14:10 Thorsten Keller, Patrick Schellhorn Florian Haftmann


Betreuung im Rechnerraum

Jeder Gruppe ist ein individueller Betreuer zugewiesen. Erfreulicherweise gibt es dieses Semester zusätzlich wieder einen studentischen Betreuer, Lukas Bulwahn, an den Sie sich im Rechnerraum wenden können, wenn Sie spontane Fragen zur Benutzung von Isabelle haben. Er ist zu folgenden Zeiten anwesend:


Mailing Liste

Es gibt unter psv bei in.tum.de eine Maillingliste, in die Sie automatisch eingetragen wurden; über diese Liste werden Neuigkeiten mitgeteilt. Auch Sie können auf dieser Liste Mitteilungen posten, die für das Praktikum relevant sind.


Arbeitsunterlagen und Aufgaben

Arbeitsunterlagen

Vorlesungsbegleitende Arbeitsunterlagen finden Sie hier.

Dokumentation

Aufgaben


Contest-Resultate

Boris Borisov und Georgi Georgiev haben den Preis für die erste abgegebene Lösung gewonnen. Es wird kein Preis für die schnellste Lösung vergeben, da alle bis jetzt abgegebenen schnellsten Lösungen sich von der Laufzeit her im Rahmen der Messgenauigkeit nicht signifikant unterscheiden (und ausserdem wesentlich langsamer als die Musterlösung sind).

Christian Varadi (varadi), Maximilian Wahler (wahlerm) 186s
Zied Tfifha (tfifha), Sebastian Zeller (zellers) 54s
Thomas Schneider (schneidt), Christoph Erdle (erdle) 51s
Boris Borisov (borisovb), Georgi Georgiev (georgiev) 52s
Matthias Häring (matthias.haering bei web.de), Lars Goldammer (lars.goldammer bei mytum.de)
Nataliya Starchenko (starchen), Christoph Mair (mair) 51s
Thorsten Keller (kellert), Patrick Schellhorn (schellho) 54s
Musterlösung (test5) 2s


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 entsprechende Rechnerraum ist 01.11.034. Um in den Rechnerraum hineinzugelangen benötigen Sie eine Chipkarte, die Sie bei der Praktikumsleitung nach der ersten Vorlesung gegen 10 Euro Pfand bekommen können.

(2) Starten von Isabelle

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

        /usr/proj/isabelle/Isabelle/bin/Isabelle
      

Mit

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

(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. 384M Arbeitsspeicher und einer 500Mhz CPU möglich. Hinweise zur Installation finden Sie hier. Installation unter Windows (auch cygwin) ist nicht zu empfehlen; als Alternative bietet sich die Isabelle Live CD IsaMorph an.

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

Zum Abschluss 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.

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, Springer Verlag, 2002.
  2. Tobias Nipkow Structured Proofs in Isar/HOL
  3. Markus Wenzel. The Isabelle/Isar Reference Manual, TU München, 2005.
  4. Lawrence C. Paulson. ML for the working programmer, Cambridge University Press, 1996.
  5. Daniel J. Velleman. How to Prove it: A Structural Approach, Cambridge University Press, 1996.

 
Steven Obua Last modified: Mon Jul 24 17:25:59 MEST 2006