Welcome to the Homepage of Jan Křetínský

Since October 2015 I am a tenure-track assistant professor at the Chair for Foundations of Software Reliability and Theoretical Computer Science, Technical University of Munich, Germany.

Contact

firstname.lastname@in.tum.de
Room: MI 03.11.044
Boltzmannstr. 3, 85748 Garching, Germany
Tel.: +49 89 289 17209
I may look like any of the guys on the right. So don't be surprised when contacting me in person:-)

Research

ha-index: 89
For h-index, see Google Scholar

Areas

probabilistic model checking
applications of machine learning in verification
temporal logics, in particular LTL and PCTL
automata theory
continuous-time stochastic processes and games
modal transition systems

Publications

See DBLP, or my CV or Google Scholar. Some full versions are accessible as technical reports not listed by DBLP. The bibtex entries can be found here.

Tools

Rabinizer 3 (developed with Zuzana Komarkova) and the previous versions Rabinizer 2 (developed with Ruslan Ledesma Garza) and Rabinizer (developed with Andreas Gaiser): tools for translation of LTL formulae to deterministic automata
MoTraS (developed with Salomon Sickert), and the old version (developed with Martin Stoll): graphical tools implementing algorithms for modal transition systems and their extensions
MoChiBA (developed with Salomon Sickert): a probabilistic LTL model checker based on semi-deterministic (limit-deterministic) automata

Community service

Events organization

Dagstuhl Seminar 18121 Machine Learning and Model Checking Join Forces, March 2018
LiVe 2018: 2nd workshop on Learning in Verification, satellite event of ETAPS 2018
LiVe 2017: 1st workshop on Learning in Verification, satellite event of ETAPS 2017

PC Member

TACAS 2018
LiVe 2018 (co-chair)
FORMATS 2017
TIME 2017
QAPL 2017
TTCS 2017
ACSD 2017
QEST 2017
LiVe 2017 (co-chair)
TACAS 2017
SOFSEM 2017
MEMICS 2016
ECAI 2016
QAPL 2015

Invited Talks

Isola 2016, WATA 2016, Mysore workshop "Trends and Challenges in Quantitative Verification" in 2016, Dagstuhl seminars in 2017 (3x), 2015, 2014, 2010

Education and previous positions

From 2013 to 2015 I was an IST Fellow at IST Austria hosted by the group of Thomas Henzinger and the group of Krishnendu Chatterjee.
I received my PhD at the Technical University Munich, Germany, where my advisor was Javier Esparza. The thesis Verification of Discrete- and Continuous-Time Non-Deterministic Markovian Systems was defended summa cum laude (with distinction). I received another PhD at Masaryk University Brno, Czech Republic, with my advisor being Antonín Kučera and my thesis Modal Transition Systems: Extensions and Analysis (with distinction). There I also received my Master's and Bachelor's degrees in computer science, mathematics, philosophy and linguistics.
My CV can be found here.

Stays

Apart from working at IST Austria, Masaryk University Brno, and Technical University Munich, I also stayed at

Aalborg University (computer science department and CISS), Denmark
(one semester in 2009, one month in 2011, two weeks in 2014),
INRIA Rennes, France
(three weeks in 2012, two weeks in 2014),
Saarland University - Computer Science , Saarbrücken, Germany
(one week in 2013, one week in 2015).

Teaching

Lectures

IN2340 Quantitative verification (Winter 2016/2017)
IN2157 Fundamental algorithms (Winter 2016/2017)
IN2148 Pearls of Informatics 1 (Winter 2016/2017)
IN2050 Model Checking (Summer 2016, 2017)
IN2007 Complexity (Summer 2016)
IN2041 Automata and Formal Languages (Winter 2015/2016)

Tutorials

Technical University Munich

IN0018 Diskrete Wahrscheinlichkeitstheorie (Summer 2012)
IN2007 Complexity (TUM, Summer 2010, 2011)
IN2041 Automata and Formal Languages (Winter 2009/10, 2010/11, 2011/12, 2012/13)

Masaryk University

IA008 Computational Logic (Spring 2009)
IB102 Automata and Grammars (Autumn 2007)
MB003 Linear Algebra and Geometry I (Spring 2008)
MB005 Foundations of mathematics (Autumn 2007)
M1110 Linear Algebra and Geometry I (Autumn 2007)

Students

PhD Students

Pranav Ashok (since 2016)
Julia Krämer (since 2017)
Tobias Meggendorfer (since 2016, also Master thesis)
Salomon Sickert (co-supervised, since 2015)
Master Students
Sebastian Fiss (Master thesis in 2017)
Matthias Franze (Master thesis in 2017)
Christopher Polster (Master thesis in 2017)
Alexej Rotar (Bachelor thesis in 2017)
Clara Waldmann (Master thesis in 2016)
Maximilian Weininger (Guided research in 2016, Master thesis in 2017)
Past Students (2010-2013)
Carlos Camino: Probabilistic Cellular Automata
Moritz Fuchs: An Advanced Solver for Presburger Arithmetic
Martin Stoll: MoTraS: A Tool for Modal Transition Systems
Salomon Sickert: Refinement Algorithms for Parametric Modal Transition Systems
Imre Vadász: Discretization of Time-Bounded Reachability in Generalized Semi-Markov Games
Dennis Kraft: Almost Sure Winning Strategies in Stochastic Real Time Games with Timed Automata Objectives
Markus Dausch: Tool for Continuous Time Stochastic Games (GUI and Simulations)
Tuan Duc Nguyen: An Extension of a Tool for Modal Transition Systems
Philipp Meyer: Algorithms for Refinement of Modal Process Rewrite Systems
Alexander Manta: Implementation of Algorithms for Modal Transition Systems with Durations
Michael Opitz: Algorithms for the Verification of Open Interactive Markov Chains

Personal

I am also interested in travelling, photography, skiing, windsurfing, volleyball, chocolate, languages etc.