Projects for Students

We offer projects suitable for

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.

Find more information here.

Development of a distributed build platform for Isabelle

Changes to existing software can often lead to unpredicted behaviour or faults, and in particular in theorem proving, changes to the inner machinery can have a large impact. In Isabelle, the Archive of Formal proofs serves as a large system test. It is thus desirable to check a large body of formalizations quickly. Build performance is best on high-speed consumer hardware; however, this comes with the drawback of little parallelization capabilities. Distributing the build onto multiple machines is thus desirable to achieve short build-times. The task of this thesis is to build an appropriate build platform to enable distribution.

Find more information here.

Clone Detection in Isabelle Theories

Duplicate code segments, or “clones,” typically arise when developers copy & paste existing code to form the basis of new code. While occasionally helpful, clones can complicate maintenance drastically, and often indicate a code quality issues. The goal of this project is to develop a tool to detect clones in formal Isabelle theories. The tool should be developed as a frontend to an existing clone detection framework, such as Moss or JCCD.

Find more information here.

Verification of Combinatorial Algorithms

The aim is to verify a library of algorithms for listing combinatorial objects: permutations, subsets, partitions, trees, … .

Find more information here.

Congruence Closure

The goal of this project is to formalize a proof-producing congruence closure algorithm. Congruence closure is an important operation in automated theorem proving that determines which terms are equal under substitutivity of equality and a given set of equalities.

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.

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.

Find more information here.

Improving Isabelle Proofs

In interactive theorem provers such as Isabelle, the system provides a collection of automatic proof methods for solving individual goals. Applications of those methods require a varying amount of user input and configuration. Consequently, proofs can often be stated differently, with different run-time and cognitive complexity characteristics. The task is to build a tool to re-write proofs into an optimized version.

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.

Query optimization for databases

Queries to relational databases frequently touch more than a hundred relations at a time. When executing those queries the order of joins between those relations is of utmost importance to the performance of the query. The goal of this project is to formalise the basis of query optimisation, i.e. query graphs and join trees. After that, one can proceed to formalise query optimisation algorithms such as the IKKBZ algorithm or dynamic programming algorithms.

Find more information here.

Theorem Dependency Mining

The theories of the Isabelle Archive of Formal Proofs (AFP) form a large dependency graph. This projects goal is to utilize graph mining techniques in order to identify useful patterns in theorem dependencies, such as lemmas that are frequently used together in proofs.

Find more information here.

Automatic Definition of Running Time Functions

The aim of this project is to automate the definition of ``running time functions’’, i.e. functions that express the complexity of another function. The automation should translate the definition of some function f in a simple functional language to an analogous function that computes the number of function calls f makes.

Find more information here.

Higher-Order Unification Hints

Unification hints are a controlled mechanism to extend unification algorithms with new inference rules. They are particularly useful for interactive theorem provers. The goal of this project is to extend the existing framework of unification hints in Isabelle to full higher-order logic and prove its usefulness by means of new tactics and case studies.

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.

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.

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.