Developer/PhD/PostDoc-position in quantitative verification or teaching automata theory

10.08.2021, Wissenschaftliches Personal

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 student in quantitative verification interested in co-developing Automata Tutor - main developer of Automata Tutor

=== ATTENTION: THIS CALL HAS BEEN ANSWERED AND THE POSITIONS FILLED. PLEASE DO NOT APPLY FOR IT ANY MORE ===


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 student in quantitative verification 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, building model checkers (also verified by automated theorem proving) etc.
- AUTOMATA TUTOR (available at [1], described in publication [2]) 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.

[1] https://automata-tutor.model.in.tum.de/
[2] https://link.springer.com/chapter/10.1007%2F978-3-030-53291-8_1


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 €50k gross and over €30k net p.a.
- Generous travel and equipment funds
- Numerous international collaboration opportunities
- 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


The call is also available at https://www7.in.tum.de/~kretinsk/positions.html
PLEASE DO NOT APPLY ANY MORE, THE POSITIONS HAVE BEEN FILLED.
[Applications online by email to jan.kretinsky@tum.de (subject = "application for position") with attached CV, transcript of records, motivation letter, and list of references]
Deadlines: the positions are to start in 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.

Kontakt: maxi.weininger@tum.de

Mehr Information

https://www7.in.tum.de/~kretinsk/positions.html