Open positions funded by the ERC grant InOVationCS (Intelligence-Oriented
Verification&Controller Synthesis) led by Prof. Jan Kretinsky:
- postdoc and PhD student positions in the area of quantitative
verification and safe&explainable AI
- scientific programmer, developer of Automata Tutor / PhD student
interested in co-developing Automata Tutor
Topics:
- QUANTITATIVE VERIFICATION: analysis of probabilistic systems (Markov
decision processes, stochastic games, chemical reaction networks), automata
theory and temporal logic, machine-learning techniques in verification,
controller synthesis, formal methods in robotics
- SAFE AND EXPLAINABLE AI: verification of machine-learnt systems such as
neural networks, analysis of systems with AI-based components,
explainability of controllers of cyber-physical systems, safe reinforcement
learning and PAC guarantees
- 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 and graded
more than a million exercise solutions.
[1] https://automata-tutor.live-lab.fi.muni.cz/
[2] https://link.springer.com/chapter/10.1007%2F978-3-030-53291-8_1
More information on the research done in our group is available at
https://live-lab.fi.muni.cz/
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 robotics applications, machine learning or
similar is 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.
Scientific programmer: Your task will be to support our research with
implementation activities.
Automata Tutor 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 group
- Dynamic and collaborative work style
- Flexible working hours, home office possibilities etc.
- Generous travel and equipment funds
- Numerous international and industrial collaboration opportunities
- The positions are based at Masaryk University Brno, Czech Republic, with
a close collaboration with the part of our group residing at TU Munich.
- Competitive salary around 1900 EUR net per month with comparatively low
cost of living in the Czech Republic
- CS department of Masaryk University is a vibrant environment, among top
10 CS departments worldwide in the area of Logic and Verification, see
https://csrankings.org/#/index?log&world
- Brno was voted the 8th most popular student city in the QS ranking and
the 4th best student city in the world according to the Campus Advisor.
For more information and for applications online, please send an email to
jan.kretinsky(a)tum.de (subject = "application for position") with attached
CV, transcript of records, motivation letter, and list of references. The
positions are to start in Autumn or as negotiated.
