Master-Praktikum: Spezifikation und Verifikation, Sommersemester 2017

Übersicht

Ablauf

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

Anmeldung

Die Anmeldung und Platzvergabe erfolgt über das Matchingsystem. Eine Vorbesprechung findet nicht statt. Melden Sie sich bitte stattdessen vorher bei Julian Brunner per E-Mail, wobei Sie kurz erläutern sollten, ob und woher Sie Isabellekenntnisse haben (z.B. durch Besuch einer der obigen Vorlesungen).

Themen

Parser Combinators

Parser combinators are a very common technique in each functional programmer's toolbox to parse text. They are usually implemented as functions mapping input to an optional result, together with higher-order functions for sequential composition, alternatives, repetition and others. Implement parser combinators in Isabelle and if necessary, provide setup for other Isabelle packages.

Advisor: Lars Hupel

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.

Advisor: Fabian Immler

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.

Advisor: Fabian Immler

Verification of an Interesting Algorithm or Data Structure

You are welcome to propose an algorithm or data structure and discuss the realizability with your advisor. Some examples of algorithms and data structures that were verified in past lab courses: Finger Trees, Skew Binomial Queues, Dijkstra's Algorithm, Conversion Between Regular Expressions and Finite Automata.

Ideas: String Search Algorithms (Boyer-Moore, Knuth-Morris-Pratt), Graph Algorithms (A*, Bellman-Ford, Kruskal)

Advisor: Peter Lammich

Optimal Binary Search Trees

Formalize and verify the construction of the optimal binary search tree given probabilities for the keys in the tree. This is a dynamic programming problem that can be solved in cubic time; Knuth improved the algorithm such that it runs in quadratic time.

Further Reading: https://en.wikipedia.org/wiki/Optimal_binary_search_tree

Advisor: Tobias Nipkow

Approximation of Definite Integrals

Isabelle's ‘approximation’ method uses interval arithmetic and various numeric techniques in order to prove estimates for real-valued expressions such as ‘arctan(2 ln(3))’ etc. It would be interesting to use this to also approximate definite integrals like ∫[0;1] x^-x dx or possibly even unbounded integrals like the one appearing in the definition of the Gamma function.

Advisor: Manuel Eberl

Matroids

Matroids are a structure generalising the idea of ‘linear independence’ of a set of vectors: certain sets of elements are called ‘independent’ and some additional properties hold (e.g. exchanging elements in independent sets). An interesting property of matroids is that a minimum-cost basis can be found with a greedy algorithm. This can be used e.g. to find the minimum spanning tree of a graph.

Advisor: Manuel Eberl