<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto"><span style="-webkit-text-size-adjust: auto;"><b>Professorship in Formal Models at Johannes Kepler University Linz</b></span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;"></span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">The Department of Computer Science at the Faculty of Engineering and Natural Sciences at Johannes Kepler University Linz invites applications for a permanent full-time position at the Institute for Formal Models and Verification (FMV) founded by Armin Biere.</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;"></span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">We are looking for candidates who work in fields like</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Formal verification or synthesis of software and hardware</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Techniques and tools of formal verification (e.g., model checking, equivalence checking, deductive verification, symbolic execution)</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Formal models and languages (e.g., logic-based languages, graph transformation systems, Petri nets, process algebra)</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Automatic reasoning and decision procedures (e.g., SAT, SMT, first-order logic, interactive theorem proving)</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Theoretical foundations of formal verification or synthesis (e.g., computational logic, complexity theory, discrete structures, game theory)</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Applications of verification and synthesis like concurrent/distributed systems, cyber-physical systems, analysis of programs and protocols, biological applications, and future technologies like quantum computing and artificial intelligence</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Model-based testing and runtime verification</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Formal analysis and verification of artificial intelligence technologies</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">• Probabilistic and statistical approaches for formal reasoning</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;"></span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">Application deadline: <span dir="ltr"><span dir="ltr">January 17, 2024</span></span>.</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;"></span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">Informal enquiries are welcome and may be sent to <span dir="ltr"><span dir="ltr">martina.seidl@jku.at</span></span>.</span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;"></span><br style="-webkit-text-size-adjust: auto;"><span style="-webkit-text-size-adjust: auto;">More information: <span dir="ltr"><span dir="ltr">https://www.jku.at/en/the-jku/work-at-the-jku/job-openings/professorship-positions/formal-methods/</span></span></span><div dir="ltr"></div></body></html>