E-Mail: firstname.lastname@tum.de
ORCID:
0000-0002-8122-2881Address: Botanická 554/68a, 602 00 Brno
Full list of Publications: DBLP or Google Scholar
Homepage of Jan Křetínský
Office: C514
E-Mail: firstname.lastname@tum.de
ORCID: 0000-0002-8122-2881
Address: Botanická 554/68a, 602 00 Brno
Full list of Publications: DBLP or Google Scholar
E-Mail: firstname.lastname@tum.de
ORCID:
0000-0002-8122-2881Address: Botanická 554/68a, 602 00 Brno
Full list of Publications: DBLP or Google Scholar
We are hiring postdocs/PhD/undergrads
on EU projects on verification&AI, in particular the ERC grant InOVationCS starting in June 2025.
on EU projects on verification&AI, in particular the ERC grant InOVationCS starting in June 2025.
I am a full professor at the Faculty of Informatics, Masaryk University, Brno, Czech Republic. I am also affiliated as a professor for Formal Methods for Software Reliability at the Chair for Foundations of Software Reliability and Theoretical Computer Science, with Technical University of Munich, Germany.
Research Areas
Neural Network Safety
Runtime Monitoring of Neural Network
We develop runtime monitors for neural networks to improve their reliability.
Abstraction of Neural Network
We abstract neural networks to improve verification speed.
Automata and Logic
Machine Learning for LTL Synthesis
We apply machine learning to the LTL synthesis problem.
Translating LTL to Automata
We design algorithms for translating LTL to different types of automata.
Explainability
Explaining Controllers via Decision Trees
We develop methods for explaining controllers with decision trees.
Explaining Controllers via Automata
We develop methods for explaining controllers via automata.
Security Analysis via Learning and Model-Checking Attack-Defense Trees
Algorithms for Stochastic Games
Value Iteration for Stochastic Games
We develop value iteration algorithms for stochastic games.
Concurrent Stochastic Games
We develop techniques for the verification of concurrent stochastic games which extend turn-based stochastic games by allowing players to select actions simultaneously in each state, reflecting more realistic scenarios of interactive agents acting concurrently.
Analysis of Probabilistic Systems
Tools
QuADTool
We provide a highly user-friendly tool for Synthesis of Cyber-security models based on the attack-tree concept. It also features interfaces to a variety of other tools and model-checkers, as well as built-in analysis for uncertain values. Additionally, the CLI can be used to learn attack-trees from logfiles or other traces.
SeQuaiA
This tool implements the semi-quantitative analysis of Chemical Reaction Networks.
SemML
In this project we develop learning-based exploration heuristics for LTL Synthesis that exploit the semantic labelling of the underlying Automaton/Game.
Owl
Owl is designed to help researches in formal methods to work with ω-words, ω-automata and LTL.
MONITIZER
We create a tool (Monitizer) that optimizes monitors on a NN for a specific task.
dtControl
Represent controllers as decision trees. Improve memory footprint, boost explainability while preserving guarantees.
Automata Tutor is an online teaching tool that aids instructors and students in large courses on automata and formal languages with many different exercise types.