Student Projects

Open Projects

We are always happy to collaborate with motivated students. Please don't hesitate to contact any team member if you are interested in one of our topics. We can supervise projects at TUM and MUNI.

Evaluation of State-of-The-Art Runtime Monitoring Techniques
(Type: BT, Mentor: Sabine Rieder)
In this project, we want to compare different runtime monitoring techniques. We want to evaluate them on several types of unseen data and datasets to investigate the performance and capabilities of the techniques. Experiments will be carried out with the help of Monitizer.
Decision Trees for Monitoring Neural Networks
(Type: BT, Mentor: Sabine Rieder)
We want to explore the possibilities of using Decision Trees as a more understandable monitor for Neural Networks, potentially in combination with other monitors.

Ongoing Projects

Master's theses

Yifei Xu:  A Framework for Evaluation of Runtime Monitors for Object Detection Neural Networks
(Mentor: Sabine Rieder)
While Object Detection Neural Networks are of high practical relevance, there is no standard way to evaluate them yet. In addition, not many monitors for this type of NN are known. In this thesis, we develop a framework to evaluate such monitors and present basic network monitoring methods.

Finished Projects

Master's theses

Maximilian Prokop:  Predicting Efficient Initial Strategies for Parity Games in LTL-Synthesis Using Machine Learning
(Mentor: Tobias Meggendorfer, 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
(Mentor: Stefanie Mohr, with Apple)
Alexander Slivinskiy:  Facilitating Experimental Analysis of Algorithms for Stochastic Games: Random Model Generation and Mining the Results
(resulted in a joint paper at ATVA'22)
Sabine Rieder:  Learning Support Vector Machines for Predicting Winning Strategies in LTL Synthesis 
(Mentor: Muqsit Azeem, resulted in a joint paper at CAV'23)
Sebastian Mair:  Improving Deep Q-Learning Using Statistical Model Checking
Emmanouil Seferis:  Safety Verification of Deep Neural Networks: Run-time Monitoring
(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
(resulted in a joint paper at ATVA'20)
Alexander Manta:  Machine Learning Guidance in Automata-Theoretic Approach for Reactive LTL Synthesis
(resulted in a joint paper at ATVA'19)
Christopher Polster:  Refinement for Game-Based Abstractions of Continuous-Space Linear Stochastic Systems
Sebastian Fiss:  Learning Methods for Parity Games and Their Application to LTL Synthesis
Matthias Franze:  A direct translation from the FGX-Fragment of LTL to Deterministic Parity Automata
Maximilian Weininger:  Heuristics For Solving Stochastic Games
(resulted in a joint paper at CAV'18)
Rupam Bhattacharya:  Leveraging Deep Learning Solutions for Predictive Maintenance of Industrial Datasets
(with BMW)
Clara Waldmann:  Translations of LTL to Parity Automata
(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
Florian J├╝ngermann:  Learning Algebraic Predicates for Explainable Controllers
(resulted in a joint paper in STTT)
Alicia Dimroth:  Neural Network Abstraction Using Principal Component Analysis
(Mentor: Stefanie Mohr)
Manuel Bildhauer:  Generation of Attack-Defense-Diagrams from Event Sequences of Previous Attacks
Mathias Jackermeier:  dtControl: Decision Tree Learning for Explainable Controller Representation
(Mentor: Maximilian Weininger, resulted in a joint paper at HSCC'20)
Christoph Weinhuber:  Learning Domain-Specific Predicates in Decision Trees for Explainable Controller Representation
(Mentor: Maximilian Weininger, resulted in a joint paper at TACAS'21)
Alexander Slivinskiy:  Solving Simple Stochastic Games with Quadratic Programming
(resulted in a joint paper at GandALF'20)
Lukas Michel:  Mean-Payoff Optimization in Modal Markov Decision Processes
(resulted in a joint paper at UAI'20)
Fabian Michel:  Parity Modal Markov Decision Processes
(resulted in a joint paper at UAI'20)
Calvin Chau:  Computing a Distribution-based Probabilistic Bisimulation
(resulted in a joint journal submission)
Emanuel Ramneantu:  Exercises on regular expressions in Automata Tutor
(resulted in a joint paper at CAV'20)
Alexej Rotar:  The Satisfiability Problem for Fragments of PCTL
(resulted in a joint paper at CONCUR'18)

Guided Research and Other Projects

Maria del Sol Barrientos Moreno:  Are Attack-Defense Trees Useful for Communicating Risk to Non-experts?
(Mentor: Florian Dorfhuber)
Philipp Klocke:  Neural Network Runtime Monitor
(with AUDI)
Maximilian Prokop:  Development of more sophisticated evaluation methods for edge classification in parity games as well as new classification methods
(Mentor: Muqsit Azeem)
Calvin Chau:  Abstraction Refinement for Neural Networks
(Mentor: Stefanie Mohr, resulted in a joint submission)
Christian Backs:  Machine Learning for Prediction of Edge Performance in LTL Synthesis
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)