Projects for Students
We offer projects suitable for
- bachelor and master thesis
- bachelor and master practical course
- interdisciplinary project
- paid work as “studentische Hilfskraft” (HiWi) with flexible conditions
The following projects are currently available:
Verification of approximation algorithms for graphs
Many basic graph theoretic problems are either NP-hard or are not known to be solved in better than impractical polynomial times. This makes solving those problems prohibitive if not impossible for real-world graphs. Approximation algorithms circumvent that by using less resources than exact algorithms, at the expense of providing only approximate solutions. In this project the student would formally verify that 1) the approximate solutions of those algorithms meet a certain quality guarantee and 2) the upper bounds on their runtimes are correct. Particularly interesting algorithms are for computing lower-bounds on (directed) graph diameters and approximate solutions to the All-Pairs-Shortest-Paths problem. Some of those algorithms are deterministic, and others have elements of randomness in them. A randomised algorithm would be more interesting from a verification perspective.
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.
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.
Focus: A Calculus for the Verification of Interactive Distributed Concurrent Systems in Isabelle
Formalization of a calculus for proving the correctness of systems of stream processing functions w.r.t. interface specifications, together with soundness and correctness proofs of the calculus.
Formalising graph theoretic results with combinatorial optimisation applications
Combinatorial optimisation algorithms and proofs of their correctness depend, in many cases, on graph theoretic results. In this project the student would formalise such graph theoretic results in Isabelle/HOL. The formalisation would build on a theory of undirected graphs developed in the context of verifying Edmond’s blossom shrinking algorithm.
Isabelle Performance Anlysis
Automated proof-search methods are ubiquitous in Isabelle proofs. As technology progresses, they become faster and more powerful. However, changing seemingly unrelated parts of the code-base can also result in slow-downs of individual methods, or possibly in specific theories. By analyzing these trends, we want to find out such trends and get alerted when problematic changes occur.
Extending the theory of line integrals or generalising it to surface integrals
Line integrals are a basic concept of integration that evolved in the context of physics, but currently has many applications. An Isabelle/HOL theory of line integrals was developed as a part of formalising Green’s theorem. In this project the student would work on extending the existing theory of line integrals by proving more of their properties, with a special focus on practically useful properties of them, like evaluation of different line integrals. A second possibility is developing a theory of surface integrals, which could be seen as a generalisation of the existing theory of line integrals.
Implementation of a Decision Procedure for Set Theory
The goal of this project is to implement a decisions procedure for a fragment of set theory. The project either starts from an existing formalisation or implements the procedure in Isabelle/ML.
Nelson-Oppen Combination of Theories
The goal of this project is to formalize the Nelson-Oppen combination of theories, a key building block of Satisfiability Modulo Theories (SMT). With this algorithm, one can combine two disjoint theories, e.g. the theory of arrays with the theory of reals.
Formalising Set Theory Based on Partial Functions
The goal of this project is to develop a formalisation of set theory, based on (partial) functions, starting from an embedding of free logic in Isabelle/HOL.
Tabulation Hashing
Tabulation hashing is a method to construct 3-independent hash families using fast efficient binary-operations. In this work the aim is to construct such hash families and verify their probabilistic properties.
Verified planning under uncertainty (i.e. (PO)MDP planning)
AI planning is the discipline aiming at building agents (i.e. computer programs) that act to achieve a certain goal, given a declarative description of the environment and the actions available to it. In practical applications, like autonomous vehicles driving, it is not possible to model the exact effects of actions. Planning in settings with uncertainty has been explored in the areas of AI, control, and operations research. In those settings the environment is commonly modelled as a factored Markov decision process (MDP) or a partially observable MDP.
Verified state space based classical planning
State space search is a successful technique to solve classical AI planning problems, i.e. deterministic problems with finite states. The main task of this project is to (partially) build a formally verified A* based planning algorithm.