Master-Praktikum: Spezifikation und Verifikation, Sommersemester 2016

Übersicht

Ablauf

Das Praktikum ist semesterbegleitend. Es wird von den Teilnehmern selbstständig ein Projekt mittels des Theorembeweisers Isabelle bearbeitet.

Anmeldung und Platzvergabe

Die Anmeldung und Platzvergabe läuft regulär über das Matchingsystem. Eine Vorbesprechung findet nicht statt. Melden Sie sich bitte stattdessen vorher unbedingt bei Lars Hupel per Mail, wobei Sie kurz erläutern sollen, ob und woher Sie Isabelle-Kenntnisse haben (z.B. durch Besuch einer der obigen Vorlesungen). Wenn Sie vorab Fragen zum Ablauf, den Themen oder anderen Aspekten haben, können Sie gern auch eine Mail schreiben.

Themen

Die Themen werden vor Beginn des Praktikums mit den Teilnehmern abgestimmt. Folgende Themenbereiche stehen hierfür zur Verfügung:

• 100 Theorems
  There is an online list of 100 famous mathematical theorems, 91 of which have been formalized in some theorem prover. Formalize one of the following problems in Isabelle: 13 (Polyhedron Formula), 90 (Stirling's formula), 98 (Bertrand's Postulate). You may follow existing formalizations in some other system.
• Parameterized branch-and-bound method with applications to numerical problems
  Implement a generic branch-and-bound method with a focus on global optimization problems (like e.g, [Narkawicz & Muñoz]). Unify existing approaches for numerical range-bounding (interval arithmetic, affine arithmetic, Taylor models) and use them as instantiations of the generic method.
• Newton iteration
  Newton's method is a simple method for finding approximations of roots of non-linear real functions. The goal is to develop a generic framework for this that can be instantiated for particular functions and connecting it with Isabelle's existing packages for interval arithmetic and Taylor models.
• Average height of a randomly built binary search tree
  Formalize the proof of the following theorem (see Cormen, Leiserson, Rivest): The average height of a binary search tree constructed by inserting n disinct elements into the empty tree (without any balancing) is O(log n).
• Decision procedure for lattices
  There is a simple decision procedure for inequalties (<=) in lattices (partial orders with infimum and supremum). Program and verify this decision procedure in Isabelle. A solution in Coq is described here.

In Einzelfällen können nach Absprache auch eigene Themenvorschläge berücksichtigt werden.