PhD/Postdoc Positions in Formal Methods, Konstanz (Germany)

The newly established research group in Formal Methods, led by TT-Prof. Emanuele D'Osualdo, is looking for motivated researchers to join our team at the University of Konstanz. We have openings for:

PhD: Full time (4 years) Salary: E 13 TV-L

Postdoc: Full time (2 years + extensions) Salary: E 13 TV-L

Closing date: Feb 15th (not strict)

Starting date: as soon as possible

Application link: https://stellen.uni-konstanz.de/jobposting/5565fce567135210cc6513eec9c509cc310366d00

Our research focuses on developing verification techniques in two main areas:

1) Probabilistic programs verification through the Bluebell logic POPL'25. Research directions include:

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

2) Logics and types for concurrency:

- Separation Logic, Iris
- Hyperproperties (based on OOPSLA'22)
- Session types (e.g. OOPSLA'22, ESOP'25)

Outstanding people with only a partial match to these topics are encouraged to apply. As a member of our team, you will have the opportunity to contribute to state-of-the-art research and interact with high-profile international collaborators (e.g. from Uni. Toronto, Cornell, MPI-SWS, Imperial, Groningen). The working language is English.

The University of Konstanz is one of the eleven Universities of Excellence in Germany, and is located in the beautiful city of Constance, by Lake Constance.

For more information, see https://www.emanueledosualdo.com/research/positions/ or contact Emanuele D'Osualdo at emanuele.dosualdo at uni-konstanz.de.