firstname.lastname@tum.de
Room: MI 03.11.044
Faculty of Informatics, Technical University of Munich
Boltzmannstr. 3,
85748 Garching,
Germany
Tel.: +49 89 289 17209
ORCID iD: 0000-0002-8122-2881
I may look like any of the guys on the right. So don't be surprised when contacting me in person:-)
Automata Tutor v3 is a teaching tool for courses on automata theory and introduction to computation
SeQuaiA performs semi-quantitative analysis of chemical reaction networks
dtControl 2.0 represents CPS controllers as decision trees, improving memory footprint and explainability while preserving guarantees
Rabinizer 4 translates LTL formulae to various (semi-)deterministic automata (previous versions 3.1 and 2) with Owl as a reusable library for developing such translations with additional infrastructure
MoChiBA is a PRISM-based probabilistic LTL model checker based on semi-deterministic (limit-deterministic) Büchi automata
MoTraS
for modal transition systems and their extensions
PET (Partial Exploration Tool, aka PRISM TUM in QComp, under development) is a probabilistic model checker for stochastic games, MDP and related models with (unbounded) reachability and mean payoff objectives, featuring also a module for statistical model checking
Projects (running)
Verified AI is a collaboration with AUDI AG on subprojects of EU H2020 Hi-Drive project.
Group-By Objectives in Probabilistic Verification (GOPro) is a DFG project 427755713.
Verified Model Checkers (VMC) is a DFG project 317422601.
Platform-Aware Synthesis of Embedded Control Software (PARSEC) is a TUM IGSSE project 10.06.
In collaboration, my PhD student Julia Eisentraut has obtained the following projects:
Proven Security for systems with human interaction (ProSec) is a project funded by the German Federal Ministry of Education and Research (Bundesministerium für Bildung und Forschung) and supported by Software Campus performed in collaboration of TUM and DATEV eG
Formal Methods for Analysis of Attack-Defence Diagrams is a PhD project of Studienstiftung des deutschen Volkes
2017: ACSD, FORMATS, LiVe (co-chair), QAPL, QEST, SOFSEM, TACAS, TIME, TTCS
2016: ECAI, MEMICS
2015: QAPL
SC Member
ETAPS (since 2021)
Invited Talks
Invited talks at conferences, workshops, summer schools
Quantitative Aspects of Variant-rich Systems (QAVS) 2022
Quantitative Logics and Automata (seminar at TU Dresden)
Modern Trends in Informatics (seminar at Brno University of Technology)
Formal Methods and Models (seminar at LaBRI) 2021
Marktoberdorf Summer School in 2021 (due to pandemics moved to 2023)
11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF) 2020
IRIF Modelling and Verification (seminar at Paris Diderot University) 2020
16th International Conference on Quantitative Evaluation of SysTems (QEST) 2019
Workshop on Security practices for Internet of Things (SPIoT) 2019
6th International Workshop on Synthesis of Complex Parameters (SynCoP) 2019
Highlights of Logic, Games and Automata (Highlights) 2018
2nd School on Foundations of Programming and Software Systems: Logic and Learning (FLOC + EATCS + SIGLOG summer school) 2018
Learning in Verification and Verification of Learning (seminar organized by the universities of Brussels and Mons) in 2018
Logic and Learning (workshop at Alan Turing Institute of data science) in 2018
Invitation-based seminars and workshops
Czech-French AI Workshop 2022
Rigorous Automated Planning (Lorentz Center Workshop) 2022
Bellairs workshop on Learning and Verification in 2019
Google Summer of Code (at Google in Munich) in 2017
Quantitative Systems: Theory and Applications (QuaSy) 2017
KiMfest 2017
Trends and Challenges in Quantitative Verification (Mysore workshop) 2016
International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola): 2016, 2018, 2020 (moved to 2021), 2022
Dagstuhl seminars:
Verification and Synthesis of Human-Robot Interaction 2019
Machine Learning and Model Checking Join Forces 2018 (co-organizer)
Formal Synthesis of Cyber-Physical Systems 2017
Game Theory in AI, Logic, and Algorithms 2017
Computer-Assisted Engineering for Robotics and Autonomous Systems 2017
Non-Zero-Sum-Games and Control 2015
Quantitative Models: Expressiveness, Analysis, and New Applications 2014
Quantitative Models: Expressiveness and Analysis 2010
Reviewing
Reviewer for journals (selection): Acta Informatica, Information Processing Letters, Journal of Automated Reasoning, Journal of Computer and System Sciences, Performance Evaluation, Software and Systems Modeling, Theoretical Computer Science, Transactions on Modeling and Computer Simulation, Transactions on Programming Languages and Systems, Transactions on Software Engineering
PhD theses:
Jakob Piribauer: On Non-Classical Stochastic Shortest Path Problems (Dresden University of Technology, Germany, 2021)
Yuliya Butkova: Towards Efficient Analysis of Markov Automata (University of Saarland, Germany, 2020)
Maxime Audinot: Assisted Design and Analysis of Attck Trees (University of Rennes 1, France, 2018)
Enno Ruijters: Zen and the Art of Railway Maintenance (University of Twente, The Netherlands, 2018)
Grant proposals:
Charles University Grant Agency
European Research Council (ERC Advanced Grants)
French National Research Agency (ANR)
German Research Foundation (DFG)
Israel Science Foundation (ISF)
Vienna Science and Technology Fund (WWTF)
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
Sudeep Kanav (planned from 2023)
Debraj Chakraborty (planned from 2023)
Sadegh Mohagheghi (planned from 2023)
Alexandros Evangelidis (since 2020)
PhD Students
Maximilian Prokop (planned from 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 (since 2019)
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 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
I am a professor for Formal Methods for Software Reliability at the Chair for Foundations of Software Reliability and Theoretical Computer Science,
Technical University of Munich, Germany.
