Jan Kretinsky

Jan Kretinsky is a full professor at the Faculty of Informatics, Masaryk University, Brno, Czech Republic, and holds an affiliated professorship at the Chair for Foundations of Software Reliability and Theoretical Computer Science at Technical University of Munich (TUM), Germany. He specializes in formal methods, focusing on verification and synthesis of probabilistic systems, applications of machine learning in verification, and explainable AI. His research bridges theoretical foundations with practical tools, including the Automata Tutor teaching platform and the Rabinizer tool for LTL-to-automata translation.

Education: PhD from TU Munich (advisor: Javier Esparza) and Masaryk University (advisor: Antonín Kučera), both with distinction. Previously an IST Fellow at IST Austria and a tenure-track assistant professor at TUM.

Research interests span verification of neural networks, probabilistic model checking, temporal logics, and automata theory. He leads the LiVe Lab and collaborates on EU projects like the ERC grant InOVationCS. Active in organizing workshops (LiVe series, Dagstuhl seminars) and serves on program committees for conferences like CONCUR, LICS, and TACAS.

Teaching includes courses on complexity, automata theory, and quantitative verification at both institutions. Supervised numerous PhD and master's students, with notable projects in decision tree controllers, runtime monitoring, and attack-defense analysis. Key grants include DFG projects (e.g., GOPro, ConVeY) and EU initiatives.

Tools developed: Automata Tutor, Rabinizer series, dtControl, SeQuaiA, and QUADTool. Research highlights include PAC guarantees for MDPs, semantic abstraction for motion planning, and formal methods for cybersecurity.