Teaching

Lectures

• IN2007 Complexity (Summer 2016, 2019)
• IN0011 Einführung in die theoretische Informatik (Summer 2018), tool Automata Tutor v3
• IN2340 Quantitative verification (Winter 2016/17, 2017/18, 2018/19, 2020/21, 2021/2022)
• IN2157 Fundamental algorithms (Winter 2016/17, 2017/18, 2018/19, 2021/2022)
• IN2148 Gems of computer science I (Perlen der Informatik 1) (Winter 2016/17, 2017/18, 2018/19, 2019/20, 2020/21, 2021/2022)
• IN2050 Model Checking (Summer 2016, 2017, 2020, 2021, 2022)
• IN2041 Automata and Formal Languages (Winter 2015/16, 2019/20)

Tutorials (past)

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)

Supervision

Post-Docs

• Kush Grover (since 2025)
• Debraj Chakraborty (since 2023)
• Sudeep Kanav (2023-2025)
• Sadegh Mohagheghi (2023-2024)
• Alexandros Evangelidis (since 2020)

PhD Students

• Maximilian Prokop (since 2023)
• Sabine Rieder (with AUDI since 2021, also Master's thesis)
• Marta Grobelna (since 2021, partially with Fraunhofer)
• Muqsit Azeem (since 2020)
• Florian Dorfhuber (since 2020)
• Stefanie Mohr (Mühlberger) (since 2020, also Master's thesis)
• Kush Grover (2019-2024)
• Maximilian Weininger: Solving Stochastic Games Reliably (since 2018, also Guided research and Master's thesis)
• Julia Eisentraut (Krämer) (since 2017, now Member of Parliament of North Rhine-Westphalia)
• Pranav Ashok: A Learning Twist on Controllers: Synthesis via Partial Exploration and Concise Representations (2016-2021, now at Fraunhofer IKS)
• Tobias Meggendorfer: Verification of Discrete-Time Markov Decision Processes (2016-2021, also Master's thesis, now at IST Austria)
• Salomon Sickert: A Unified Translation of Linear Temporal Logic to Omega-Automata (informally co-supervised, 2015-2019, also Bachelor's thesis, now at Hebrew University of Jerusalem)

Master's Theses

• Maximilian Prokop: Predicting Efficient Initial Strategies for Parity Games in LTL-Synthesis Using Machine Learning (2022; resulted in a joint paper at CAV'23)
• Calvin Chau: Raising the Abstraction Level of Hardware Model Checking by Generating Verification Code from Activity Diagrams (2022, with Apple)
• Alexander Slivinskiy: Facilitating Experimental Analysis of Algorithms for Stochastic Games: Random Model Generation and Mining the Results (2022; resulted in a joint paper at ATVA'22)
• Sabine Rieder: Learning Support Vector Machines for Predicting Winning Strategies in LTL Synthesis (2021; resulted in a joint paper at CAV'23)
• Sebastian Mair: Improving Deep Q-Learning Using Statistical Model Checking (2021)
• Emmanouil Seferis: Safety Verification of Deep Neural Networks: Run-time Monitoring (2020, with AUDI and prof. Knoll; resulted in a joint paper at RV'21)
• Stefanie Mühlberger (Mohr): Faster Verification of Neural Networks with Clustering-based Compression (2020; resulted in a joint paper at ATVA'20)
• Alexander Manta: Machine Learning Guidance in Automata-Theoretic Approach for Reactive LTL Synthesis (2019; resulted in a joint paper at ATVA'19)
• Christopher Polster: Refinement for Game-Based Abstractions of Continuous-Space Linear Stochastic Systems (2019)
• Sebastian Fiss: Learning Methods for Parity Games and Their Application to LTL Synthesis (2018)
• Matthias Franze: A direct translation from the FGX-Fragment of LTL to Deterministic Parity Automata (2018)
• Maximilian Weininger: Heuristics For Solving Stochastic Games (2017; resulted in a joint paper at CAV'18)
• Rupam Bhattacharya: Leveraging Deep Learning Solutions for Predictive Maintenance of Industrial Datasets (2017, with BMW)
• Clara Waldmann: Translations of LTL to Parity Automata (2016; resulted in a joint paper at TACAS'17)

Bachelor's Theses

• Alexander Taepper: Containing the State Space Explosion in the Model Checking of Attack-Defense Trees (2022)
• Florian Jüngermann: Learning Algebraic Predicates for Explainable Controllers (2021; resulted in a joint paper in STTT)
• Alicia Dimroth: Neural Network Abstraction Using Principal Component Analysis (2021)
• Manuel Bildhauer: Generation of Attack-Defense-Diagrams from Event Sequences of previous Attacks (2020)
• Mathias Jackermeier: dtControl: Decision Tree Learning for Explainable Controller Representation (2020; resulted in a joint paper at HSCC'20)
• Christoph Weinhuber: Learning Domain-Specific Predicates in Decision Trees for Explainable Controller Representation (2020; resulted in a joint paper at TACAS'21)
• Alexander Slivinskiy: Solving Simple Stochastic Games with Quadratic Programming (2020; resulted in a joint paper at GandALF'20)
• Lukas Michel: Mean-Payoff Optimization in Modal Markov Decision Processes (2020; resulted in a joint paper at UAI'20)
• Fabian Michel: Parity Modal Markov Decision Processes (2019; resulted in a joint paper at UAI'20)
• Calvin Chau: Computing a Distribution-based Probabilistic Bisimulation (2019; resulted in a joint journal submission)
• Emanuel Ramneantu: Exercises on regular expressions in Automata Tutor (2019; resulted in a joint paper at CAV'20)
• Alexej Rotar: The Satisfiability Problem for Fragments of PCTL (Bachelor thesis in 2018; resulted in a joint paper at CONCUR'18)

Guided Research and Others

• Maria del Sol Barrientos Moreno: Are Attack-Defense Trees Useful for Communicating Risk to Non-experts? (2022)
• Philipp Klocke: Neural Network Runtime Monitor (with AUDI; 2021)
• Maximilian Prokop: Developement of more sophisticated evaluation methods for edge classification in parity games as well as new classification methods (2021)
• Calvin Chau: Abstraction Refinement for Neural Networks (2021; resulted in a joint submission)
• Christian Backs: Machine Learning for Prediction of Edge Performance in LTL Synthesis (2020)
• Maximilian Weininger: Translating Linear Temporal Logic to Parity Automata (guided research in 2016; resulted in a joint paper at TACAS'17)
• Christopher Ziegler (Google Summer of Code in 2016; resulted in a joint paper at CAV'18)

Past Bachelor's Theses (advisor 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