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@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.