[TYPES/announce] PhD/PostDoc positions in Formal Methods at the University of Konstanz (Germany)

[Emanuele D'Osualdo]

Please distribute (apologies for multiple postings):
=====================================

PhD/PostDoc positions in Formal Methods at the University of Konstanz (Germany)
https://urldefense.com/v3/__https://www.emanueledosualdo.com/research/positions/__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTvJhczdZ$ 

=====================================

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://urldefense.com/v3/__https://stellen.uni-konstanz.de/jobposting/5565fce567135210cc6513eec9c509cc310366d00__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTo301c_U$ 

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

 * Probabilistic programs verification through
   the Bluebell logic [POPL'25](https://urldefense.com/v3/__https://doi.org/10.1145/3704894__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTnQLg8MS$ ).
   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

 * Logics and types for concurrency:
   - Separation Logic, Iris
   - Hyperproperties (based on [OOPSLA'22](https://urldefense.com/v3/__https://doi.org/10.1145/3563298__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTo_s8DH3$ ))
   - Session types (e.g. [OOPSLA'22](https://urldefense.com/v3/__https://doi.org/10.1145/3563318__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTjdqwqcp$ ), [ESOP'25](https://urldefense.com/v3/__https://arxiv.org/abs/2501.16977__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTpGSsItJ$ ))

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.

Please reach out to Prof. Emanuele D’Osualdo at emanuele.dosualdo at uni-konstanz.de for any questions.
For more info: https://urldefense.com/v3/__https://www.emanueledosualdo.com/research/positions/__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTvJhczdZ$ 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20250130/ed5dd133/attachment-0001.htm>