Open positions in verification at TUM

Positions in the Formal Methods for Software Reliability group of TU Munich led by Prof. Jan Kretinsky

postdoc in the area of quantitative verification
PhD students in quantitative verification and verified AI, possibly interested in co-developing Automata Tutor
main developer of Automata Tutor

Topics:

QUANTITATIVE VERIFICATION: analysis of probabilistic systems (Markov decision processes, stochastic games, chemical reaction networks), automata theory and temporal logic, machine learning in verification and verification of machine-learnt systems such as neural networks (also in industrial cooperation with AUDI), building model checkers (also verified by automated theorem proving) etc.
AUTOMATA TUTOR (available here, described in publication at CAV'20) is a tool to teach undergraduate students the basics of theoretical computer science. It offers automatic grading and feedback of various types of exercises. The tool has been used at dozens of universities around the world (including 5 times at TUM) and graded almost a million exercise solutions.

Requirements:
We are looking for highly motivated candidates who will fit our enthusiastic and collaborative group spirit.

Post-doc: The applicant is expected to have a solid publication record in theoretical CS. Experience with biological applications, robotics applications, or machine learning is also appreciated.

PhD: The candidate is expected to have some background in theoretical computer science, including some of the following areas: automata, logic, games, verification/model checking, probabilistic or timed systems, automated theorem proving (Isabelle, Coq). Besides, we strongly appreciate experience with developer activities as described below.

Developer: Your tasks will include making Automata Tutor an open-source project, supervising deployment, and improving the tool by developing and implementing user-stories. Additionally, we are interested in analyzing the student solutions using machine learning.

We offer:

International and gender-balanced group
Dynamic and collaborative work style
Flexible working hours, home office possibilities etc.
Full-time research position on the (standard German) TV-L E13 pay scale, i.e. over EUR 50k gross and over EUR 30k net p.a.
Generous travel and equipment funds
Numerous international collaboration opportunities
Industrial collaboration opportunities, in particular with AUDI
CS department of TU Munich is a vibrant international environment, regularly among top 30 CS departments worldwide
Munich is regularly among the very top cities w.r.t. the quality of life

Applications online by email to jan.kretinsky@tum.de (subject = "application for position") with attached CV, transcript of records, motivation letter, and references.
Deadlines: the positions are to start in Summer, Autumn or as negotiated; applications are due by Sep 13 but may continue until the positions are filled.

Please contact jan.kretinsky@tum.de for any further information.