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 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.
Projects (previous)
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
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
Rigorous Automated Planning (Lorentz Center Workshop) 2022
9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola) 2020 (moved to 2021)
Bellairs workshop on Learning and Verification in 2019
8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola) 2018
Google Summer of Code (at Google in Munich) in 2017
Quantitative Systems: Theory and Applications (QuaSy) 2017
KiMfest 2017
7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (Isola) 2016
Trends and Challenges in Quantitative Verification (Mysore workshop) 2016
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)
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.
