Research Positions
I am looking for enthusiastic and motivated students and postdocs to join my group at the University of Konstanz. We currently offer:
-
1 PhD position:
Full time (4 years)
Salary: E 13 TV-L 100% -
1 Postdoc position:
Full time (2 years + extensions)
Salary: E 13 TV-L 100%
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
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 in ongoing work with Felix Stutz.