Projects for Students

We offer projects suitable for

The following projects are currently available.

Automatic Laurent Series Expansions

Sufficiently nice complex-valued functions admit Laurent series expansions, which can be computed symbolically. This is an important feature in Computer Algebra Systems like Mathematica that can be used to e.g. compute limits and complex residues. In this Master's thesis project, a procedure is developed that computes such Laurent series inside the proof assistant Isabelle/HOL to aid the user by automatically proving limits, residues, and reasoning about poles.
Find more information here.

Testing with a verified oracle: using Symbolic Execution and Fuzzing

There is quite a large collection of formally verified algorithms in Isabelle. The idea of this project is to utilize these provably correct algorithms as oracles when testing real-world programs that implement the same algorithm. Symbolic Execution and Fuzzing could be used to generate new inputs used in this methodology.
Find more information here.

Ein Testrahmen für funktionale Datenstrukturen

Es soll ein Testrahmen implementiert und ausgewertet werden, um die Effizienz funkionaler Datenstrukturen messen zu können. Dabei soll das Lastprofil, also der Mix der verschiedenen Operationen, flexibel spezifizierbar sein. Sodann sollen eine Reihe effizienter funktionaler Datenstrukturen für Suchbäume und Prioritätswarteschlangen implementiert und mit Hilfe dieses Testrahmens auf ihre Effizienz hin untersucht werden.
Find more information here.

Efficient Algorithms and Data Structures in Isabelle/HOL

The goal of this project is to formalize some algorithm (e.g. the blossom algorithm for maximal cardinality matching, algorithm for closest pair of points,...) or efficient data structure in Isabelle/HOL and use refinement techniques to refine the algorithm down to efficiently executable code.
Find more information here.

Numerical Proof Procedures in Isabelle/HOL

The Isabelle theorem prover can prove variable-free arithmetic statements automatically, for example arctan 1.5 < 1. The proof procedure uses Taylor polynomials and interval arithmetic. It should be extended to support more operations or make use of IEEE floating point numbers.
Find more information here.

Efficient Functional Data Structures

Mittels Codegenerierung können aus Spezifikationen unmittelbar Prototypen in einer funktionalen Programmiersprache erzeugt werden, z.B. in ML, in Haskell, oder in (einer Teilmenge von) Scala. Um die Effizienz dieser Prototypen zu steigern, sind effiziente Datenstrukturen erforderlich. Bekannte Beispiele hierfür sind balancierende Suchbäume (z.B. 2-3-Bäume); es gibt aber noch viel mehr Kandidaten. Eine Auswahl hiervon soll als Isabelle-Theorie implementiert und gegen eine naive Referenzimplementierung verifiziert werden.
Find more information here.

Clone Detection in Isabelle Theories

Duplicate code segments, or “clones,” typically arise when developers simply copy & paste existing code to form the basis of new code. This practice complicates maintenance, because each bug fix in one such segment must normally be replicated in the other similar segments. The goal of this project is to develop a tool to detect clones in Isabelle theories. The tool should be developed as a frontend to an existing clone detection framework, such as ConQAT and JCCD.
Find more information here.

SAT Solver in ML

SAT-Löser (SAT solvers) sind Programme, die erfüllende Belegungen für aussagenlogische Formeln berechnen. Ziel der Arbeit ist es, einen SAT Löser in (Standard) ML zu entwerfen und programmieren. (OCaml ist ein Dialekt von ML.) Dabei ist zu untersuchen, wie Implementierungstechniken von C sich auf ML übertragen lassen, wobei ML auch Arrays und Zeiger hat. Ausgangspunkt ist der in C geschriebene open source SAT-Löser MiniSat.
Find more information here.

This list may be incomplete, and we are open to suggestions. If you have questions concerning a specific project, simply send an email to the project's supervisor. For general questions, contact Prof. Nipkow.