<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title></title>
</head>
<body>
<div name="messageBodySection">
<div>Please distribute (apologies for multiple postings):<br />
=====================================</div>
<div> </div>
<div>PhD/PostDoc positions in Formal Methods at the University of Konstanz (Germany)<br />
<a href="https://urldefense.com/v3/__https://www.emanueledosualdo.com/research/positions/__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTvJhczdZ$">https://www.emanueledosualdo.com/research/positions/</a></div>
<div> </div>
<div>=====================================</div>
<div> </div>
<div>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:</div>
<div> </div>
<div> * PhD: Full time (4 years)<br />
Salary: E 13 TV-L</div>
<div> </div>
<div> * Postdoc: Full time (2 years + extensions)<br />
Salary: E 13 TV-L</div>
<div> </div>
<div>Closing date: Feb 15th (not strict)<br />
Starting date: as soon as possible<br />
Application link: <a href="https://urldefense.com/v3/__https://stellen.uni-konstanz.de/jobposting/5565fce567135210cc6513eec9c509cc310366d00__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTo301c_U$">https://stellen.uni-konstanz.de/jobposting/5565fce567135210cc6513eec9c509cc310366d00</a></div>
<div> </div>
<div>Our research focuses on developing verification techniques in two main areas:</div>
<div> </div>
<div> * Probabilistic programs verification through<br />
the Bluebell logic [POPL'25](<a href="https://urldefense.com/v3/__https://doi.org/10.1145/3704894__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTnQLg8MS$">https://doi.org/10.1145/3704894</a>).<br />
Research directions include:<br />
- Generalizations of the Bluebell model<br />
- Mechanization in Rocq/Iris<br />
- Applications to verification of cryptographic protocols<br />
- Automatic proof search<br />
- Extensions to handle Quantum programs</div>
<div> </div>
<div> * Logics and types for concurrency:<br />
- Separation Logic, Iris<br />
- Hyperproperties (based on [OOPSLA'22](<a href="https://urldefense.com/v3/__https://doi.org/10.1145/3563298__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTo_s8DH3$">https://doi.org/10.1145/3563298</a>))<br />
- Session types (e.g. [OOPSLA'22](<a href="https://urldefense.com/v3/__https://doi.org/10.1145/3563318__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTjdqwqcp$">https://doi.org/10.1145/3563318</a>), [ESOP'25](<a href="https://urldefense.com/v3/__https://arxiv.org/abs/2501.16977__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTpGSsItJ$">https://arxiv.org/abs/2501.16977</a>))</div>
<div> </div>
<div>Outstanding people with only a partial match to these topics are encouraged to<br />
apply. As a member of our team, you will have the opportunity to contribute to<br />
state-of-the-art research and interact with high-profile international<br />
collaborators (e.g. from Uni. Toronto, Cornell, MPI-SWS, Imperial, Groningen).<br />
The working language is English.</div>
<div> </div>
<div>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.</div>
<div> </div>
<div>Please reach out to Prof. Emanuele D’Osualdo at <a href="mailto:emanuele.dosualdo@uni-konstanz.de">emanuele.dosualdo@uni-konstanz.de</a> for any questions.<br />
For more info: <a href="https://urldefense.com/v3/__https://www.emanueledosualdo.com/research/positions/__;!!IBzWLUs!Uxh0cTe_zHb4W7n1FZxrwqiJbdgpg9INUZ1NGGfwYj7MeJkZatjh5TEMVKZYqkt5kKxG99rWTt4ASVRlUKkbPdJBQRGL_q0VTvJhczdZ$">https://www.emanueledosualdo.com/research/positions/</a><br />
</div>
</div>
</body>
</html>