Matthias Volk

Email

matthias.volk@cs.rwth-aachen.de

Address

Room 4205
Ahornstraße 55
D-52074 Aachen

Phone

+49 241 80 21212

This website is outdated!

Please see my personal website.

Research

I am a PhD student at the Software Modeling and Verification Group (MOVES) headed by Professor J.-P. Katoen since December 2015. I was a doctoral researcher (Stipendiat) within the Research Training Group UnRAVeL since 2017. Since 2020 I am part of the ERC research project FRAPPANT.
My research interests include:

• Analysis of dynamic fault trees (DFTs)
• Verifiying fault trees for railway safety (see UnRAVeL project AP4)
• Model checking of (parametric) probabilistic systems

Tool support

I am actively involved in the development of the following tools:

• The probabilistic model checker Storm and its python bindings stormpy
• The python bindings pycarl for the arithmetic library CArL
• The parameter synthesis framework for parametric Markov chains PROPhESY

Bachelor/Master Theses

I am always looking forward to work with students. If you are looking for a thesis in one of the areas above, do not hesitate to contact me and we can discuss current thesis topics. Some ideas are also given in our list of open topics.

Currently, I am supervising the following theses:

• Daniel Basgöze, Dynamic Fault Tree Analysis using Binary Decision Diagrams, Bachelor thesis (together with Shahid Khan)
• Markus Miliats, Analyzing critical components in Dynamic Fault Trees, Bachelor thesis

In the past, I have been supervising the following theses:

• Fynn Mazurkiewicz, Parameter Synthesis for Continuous-Time Markov Chains, 2020, Bachelor thesis
• Hannah Mertens, Repairs in Dynamic Fault Trees: a Petri net semantics, 2019, Bachelor thesis
• Alexander Bork, Analysing Dynamic Fault Trees by GSPNs, 2018, Bachelor thesis
• Christopher Lösbrock, Implementing an Incremental Solver for Difference Logic, 2018, Bachelor thesis (together with Gereon Kremer)
• Dustin Jungen, Repairs in Dynamic Fault Trees, 2017, Bachelor thesis (together with Sebastian Junges)
• Michael Deutschen, GSPN Semantics for Dynamic Fault Trees, 2017, Master thesis (together with Sebastian Junges)
• Ronja Nocon, Pattern-based detection of Monotonicity in Dynamic Fault Trees, 2016, Bachelor thesis (together with Sebastian Junges)

Teaching

I am currently involved in the following teaching activities:

• Probabilistic Models of Concurrency (Seminar) (SS 20)

Past teaching activities:

• Formal Semantics of Programming Languages (Seminar) (WS 19/20)
• Formale Systeme, Automaten, Prozesse (SS 19)
• Compiler Construction (WS 18/19)
• Trends and Pearls of Model Checking (Seminar) (WS 18/19)
• Introduction to Model Checking (SS 18)
• Formal Verification Meets Machine Learning (Seminar) (SS 18)
• Theoretical Foundations of the UML (WS 17/18)
• Programming Language Design and Implementation (Seminar) (WS 17/18)
• Compiler Construction (SS 17)
• Verification and Static Analysis of Software (Seminar) (SS 17)
• Advanced Model Checking (WS 16/17)
• Advances in Model Checking (Seminar) (WS 16/17)
• Compiler Construction (SS 16)
• Theoretical Foundations of Programming Languages (Seminar) (SS 16)

Awards

Our paper A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas (joint work with Norman Weik, Joost-Pieter Katoen and Nils Nießen) won the Best Paper Award at the 24th International Conference on Formal Methods for Industrial Critical Systems (FMICS) in Amsterdam in 2019. The paper presents a model of railway station areas in terms of dynamic fault trees (DFTs). The DFT model is used to assess the reliability of the infrastructure elements in the station area and the influence of infrastructure failures on the routability options of trains.

Our paper Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms (joint work with Saba Aflaki, Borzoo Bonakdarpour, Joost-Pieter Katoen and Arne Storjohann) won the Prof. C.V. Ramamoorthy Best Paper Award at the 36th IEEE Int. Symposium on Reliable Distributed Systems (SRDS) in Hongkong in 2017. The paper presents automated techniques to find the probability distribution that achieves minimum average recovery time for randomized distributed self-stabilizing algorithms.

Publications

All records on RWTH Publications