Intro

Below, we are collecting possible thesis topics (for bachelor and/or master).

It is important to understand that these are just a selection of possibly interesting research questions, it is possible to do thesis topics on different topics, too, and to take the topics below just as an inspiration.

Some topics are also more an indication of a general area of topics.

Topics

Quantum Strongest Postcondition

To verify a (quantum) program behavior, Hoare triples are used. A well-studied concept in this setting is the weakest precondition transformer, which computes the most general precondition ensuring that a given postcondition holds after program execution. Similarly, one can define the strongest postcondition, which describes the most precise characterization of the states obtained after executing a quantum program from any state satisfying a given precondition. In this thesis, we aim to formally define the strongest postcondition for quantum programs, figure out how it can be computed for a concrete (theoretical) quantum programming language and show its relationship with weakest preconditions. It is also interesting to study diverging loops and if it is possible to define a quantitative version (similar to Quantitative Strongest Post).

Supervisor: Christina Gehnen

Ideal background: Quantum computing, (program) logics

Level: Bachelor

Precise complexity of the compressed oracle

In quantum cryptography, the “compressed oracles” (going back to Zhandry’s paper), it a powerful technique to reason about random-oracles, which in turn are a widely used modeling of hash functions. While the compressed oracle has a reasonably simple abstract description which is enough for many cryptographic proofs, for some proofs we need to know how efficient/inefficient it is to actually implement a compressed oracles as a quantum algorithm. The goal of this thesis would be to study efficient algorithms for implementing the compressed oracle to find out what the complexity of it actually is. This would include several (or all) of the following tasks:

Identification and use of suitable quantum datastructures
Design of the algorithm
Runtime analysis of the algorithm
Demo implementation
Formal verification that the algorithm does what it should

Supervisor: Dominique Unruh

Ideal background: Quantum computing, programming (from the theory point of view), algorithms, datastructures.

Level: Master

Something with theorem proving

Isabelle/Coq/Lean/etc.

Easycrypt/qrhl-tool/etc.

(Description follows.)

Decision procedures for quantum references

In a recent work of mine, I introduced the concept of quantum references. This is a theoretical tool for the use in quantum programming semantics and quantum program logics to meaningfully refer to a subsystem of quantum system (a formalization of what a “wire” is in a quantum circuit, so to say). In an ongoing project in the theorem prover Isabelle/HOL (qrhl-tool), I am using quantum references to reason about program variables and operations on them etc. This leads to a lot of questions that need to be checked automatically by the computer, e.g., whether a given construction built from individual references is a reference again, whether one reference is a strict superset of another reference, etc.

The topic of this thesis would be to develop decision procedures (algorithms) for answering all those questions and to implement them (preferably in Standard/ML, inside Isabelle/HOL).