Projects for Students

We offer projects suitable for

The following projects are currently available.

A Linter for Isabelle

In this project, the student should implement a linter for Isabelle [5] in Isabelle/Scala. A linter is a program that checks the source code for patterns that are undesirable. Undesirable patterns in Isabelle could be automated proofs that are prone to break after making small changes or more trivial things such as incorrect indentation with respect to some style guide. The linter should provide an interface to define lints, switching lints on and off both globally and locally, and a way to report the lints both in a human and a machine-readable format.
Find more information here.

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.
Find more information here.

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. Examples of interesting topics to formalise there are:

  • proving Tutte's theorem and the Berge-Tutte formula,
  • studying ear-decompositions of graphs and their relationship to factor-critical graphs, and
  • studying the properties of laminar families.

Find more information here.

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.
Find more information here.

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. Tasks in this project include

  • formalising existing heuristics for classical planning in Isabelle/HOL and verifying that they are admissible. There are many such heuristics, and they are reviewed in sections 2.3 and 2.7.9 in a book by Gallab et al. [1]. A first step is to verify abstraction based heuristics like pattern databases and/or merge-and-shrink.
  • integrating an existing Isabelle formalisation of A* with 1) already formalised semantics of planning problems to obtain a version of A* that operates on planning state spaces and 2) planning heuristics that are verified.
  • refining the integrated A* to executable code.
Find more information here.

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. Tasks in this project include

  • extending the existing Isabelle formalisation of MDPs to include the notion of agent rewards
  • formalising the notion of (optimal) strategies, verifying algorithms that solve these problems, like policy/value iteration
  • refining the verified algorithm to executable code using the existing Isabelle refinement framework.
Find more information here.

Group Theory

The purpose of this project is to add various missing bits of group theory to HOL-Algebra, with a particular focus on finite groups. Topics of interest include:

  • Decomposition of a group into an interior direct product
  • Indexed direct products
  • The fundamental theorem of finite(ly generated) abelian groups
  • Finite simple groups
Find more information here.

Analytic Number Theory

There is an ongoing effort to formalise Tom Apostol's classic textbook on Analytic Number Theory. Most of the core content has already been formalised, but there are some chapters that have been left out completely, e.g. Number Partitions.

The goal of the practical course work would be to formalise as much as possible of this material.

Find more information here.

Primality Testing

There are many different tests to determine if a natural number is prime. Most of these are *probabilistic* and always recognise a prime number as prime, but, with some probability, also mistakenly classify composites as primes. Some of these tests (Fermat, Miller–Rabin, Solovay–Strassen) are already formalised in Isabelle.

In this project, more primality tests are to be formalised, e.g.:

  • Frobenius test (randomised)
  • Lucas and Fibonacci pseudoprimes (randomised)
  • Lucas–Lehmer test for Mersenne primes (deterministic)
  • AKS test (deterministic)
Find more information here.

Specialised Mathematical Tactics and Simprocs

The goal is to implement various additional tactics and/or simplification procedures ('simprocs') to simplify/expand certain mathematical terms that are difficult to simplify using simp rules (e.g.: proving/disproving/rewriting statements like "4/3 ∈ ℤ", k-th integer root and k-th power testing ,...). Some of these can be done using externally-computed certificates (e.g.: primality: Pratt certificate, prime power: prime factor (with Pratt certificate) and multiplicity, compositeness: two non-trivial factors, ...)

Proofs of concepts for some of these already exist (e.g. in the Pratt_Certificate and Bertrands_Postulate AFP entries). The goal would be to make a bigger collection of fast and robust tactics/simprocs.
Find more information here.

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.

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.