Research Positions

I am looking for enthusiastic and motivated students and postdocs to join my group at the University of Konstanz. We currently offer:

Topics

Our group focuses on formal verification techniques, for mainly two domains: probabilistic programs, and concurrent programs.

Verification of probabilistic programs

Our recent paper on the logic called Bluebell showed a promising approach to unify and extend various abstractions used for probabilistic reasoning.

This work opens a number of research directions:

• Generalizations of the model
• Mechanization in Rocq/Iris
• Applications to verification of cryptographic protocols
• Automatic proof search
• Extensions to handle Quantum programs

The work on Bluebell stemmed from our work on verifying Hyperproperties

which is also of interest to the group.

Verification of concurrent systems

Our group studies proof techniques for the compositional analysis of concurrent system through two main tools: concurrent separation logic (e.g. Iris), and types.

For example, the TaDA Live logic provided an expressive compositional way to reason about fine-grained concurrent algorithms:

On the types side, session types provide a nice compositional abstraction for protocols in concurrent systems. We explored connections with separation logic through Curry-Howard isomorphisms:

We are also working on Multi-party Session Types: