Academic Career and Research Areas

Jan Křetínský (b. 1984) works in the area of formal methods. He develops methods and tools for finding errors in software systems and proving their absence and evaluates and optimizes the performance of stochastic and real-time systems. His work also involves the verification and synthesis of safe and correct controllers. To this end, automata theory, logic, probability theory and other techniques of theoretical computer science as well as machine learning are employed.

Kretinsky studied computer science, mathematics, philosophy and linguistics at Masaryk University in Brno in the Czech Republic. He studied for his doctorate in Brno and at TUM, graduating with distinction (summa cum laude) in 2013. Afterwards he joined the Institute of Science and Technology Austria as an IST Fellow. Since 2015 he has been an assistant professor at TUM.

Brázdil T, Chatterjee K, Chmelík M, Forejt V, Křetínský J, Kwiatkowska MZ, Parker D, Ujma M: "Verification of Markov Decision Processes Using Learning Algorithms". In: Automated Technology for Verification and Analysis (ATVA). Editors: Cassez F, Raskin JF: Springer, 2014: 98-114.

Abstract

Esparza J, Křetínský J: “From LTL to Deterministic Automata: A Safraless Compositional Approach”. In: Computer Aided Verification (CAV). Editors: Biere A, Bloem R. Springer, 2014: 192-208.

Abstract

Brázdil T, Forejt V, Krčál J, Křetínský J, Kučera A: “Continuous-time stochastic games with time-bounded reachability”. Information and Computation. 2013; 224: 46-70.

Abstract

Chatterjee K, Gaiser A, Křetínský J: “Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis”. In: Computer Aided Verification (CAV). Editor: Sharygina N, Veith H. Springer, 2013: 559-575.

Abstract

Beneš N, Křetínský J, Larsen KG, Srba J: “On determinism in modal transition systems”. Theoretical Computer Science. 2009; 410(41): 4026-4043.

Abstract

If you wish your profile to be changed or updated please contact Franz Langer.