Matthias Volk

Email: matthias.volk at 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

2022
DOI	Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. The probabilistic model checker STORM, 589-610, Springer, 2022.
DOI	Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Saba Aflaki. Synthesizing optimal bias in randomized self-stabilization, 37-57, Springer, 2022.
2021
DOI	Shahid Khan, Matthias Volk, Joost-Pieter Katoen, Alexis Braibant, Marc Bouissou. Model Checking the Multi-Formalism Language FIGARO, 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks : DSN 2021 : proceedings : 21-24 June 2021, virtual event / general chairs: Sy-Yen Kuo (National Taiwan University, Taiwan), Yennun Huang (Academia Sinica, Taiwan) ; publication chairs: Chi-Yi Lin (Tamkang University, Taiwan), Yao-Hsin Chou (National Chi Nan University, Taiwan) ; publisher: IEEE, 463-470, IEEE, 2021.
DOI	Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Ahmad Zafar, Falak Sher. Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees, 2021 10th Latin-American Symposium on Dependable Computing (LADC) : proceedings : virtual conference, 22-26 November 2021 / publisher: IEEE ; general chair: Antônio Augusto Fröhlich (UFSC), publication chair: Augusto José Venâncio Neto (UFRN), IEEE, 2021.
2020
	Joost-Pieter Katoen, Martin Ritzert, Richard Marlon Wilke, Katrin M. Dannert, Peter Lindner, Dennis Fischer, Janosch Fuchs, Björn Frederik Tauer, Vipin Ravindran Vijayalakshmi, Laura Vargas Koch, Nadine Friesen, Andreas Gabriel Klinger, Marcel Tobias Hark, Benjamin Lucien Kaminski, Sebastian Junges, Jip Josephine Spel, Anton Pirogov, Stefan Schupp, Till Hofmann, Daxin Liu, Martin Comis, Tabea Claudia Krabs, Stephan Zieger, Rebecca Haehn, Matthias Volk, Norman Weik, Helene-Maria Bolke-Hermanns. UnRAVeL Research Training Group : Uncertainty and Randomness in Algorithms, Verification, and Logic, 85 Seiten, 2020.
2019
DOI	Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Safety analysis for vehicle guidance systems with dynamic fault trees, 37-50, Elsevier Science, 2019.
DOI	Matthias Volk, Norman Weik, Joost-Pieter Katoen, Nils Nießen. A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas, Formal methods for industrial critical systems ; 24th international conference, FMICS 2019, Amsterdam, The Netherlands, August 30-31, 2019 : proceedings / Kim Guldstrand Larsen, Tim Willemse (eds.), 40-58, Springer, 2019.
DOI	Yassmeen Elderhalli, Matthias Volk, Osman Hasan, Joost-Pieter Katoen, Sofiène Tahar. Formal Verification of Rewriting Rules for Dynamic Fault Trees, Software Engineering and Formal Methods : 17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019 : Proceedings / Peter Csaba Ölveczky, Gwen Salaün (Eds.), 513-531, Springer, 2019.
DOI	Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Marc Bouissou. Synergizing Reliability Modeling Languages: BDMPs without Repairs and DFTs, 2019 IEEE 24th Pacific Rim International Symposium on Dependable Computing : PRDC 2019 : Kyoto, Japan, 1-3 December 2019 : proceedings / sponsors PRDC 2019: IEEE Computer Society, Tokyo Metropolitan University, Hiroshima University, Kyoto Sangyo University, Nihon University, 266-275, IEEE, 2019.
2018
DOI	Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques, 370-379, IEEE, 2018.
DOI	Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk. One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs, Application and theory of petri nets and concurrency : 39th international conference, PETRI NETS 2018, Bratislava, Slovakia, June 24-29, 2018 : proceedings / Victor Khomenko, Olivier H. Roux (eds.), 272-293, Springer, 2018.
2017
DOI	Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A storm is Coming: A Modern Probabilistic Model Checker, 14 Seiten : Tabellen, Diagramme, 2017.
DOI	Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker, Computer aided verification : 29th International Conference, CAV 2017 : Heidelberg, Germany, July 24-28, 2017 : proceedings / Rupak Majumdar, Viktor Kunčak (eds.). - Part 2, 592-600, Springer, 2017.
DOI	Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems, Computer safety, reliability, and security : 36th International Conference, SAFECOMP 2017, Trento, Italy, September 13-15, 2017 : proceedings / Stefano Tonetta, Erwin Schoitsch, Friedemann Bitsch (eds.), 3-19, Springer, 2017.
DOI	Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Arne Storjohann. Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms, 2017 IEEE 36th International Symposium on Reliable Distributed Systems : SRDS 2017 : 26-29 September 2017, Hong Kong : proceedings / sponsored by: IEEE, IEEE Computer Society, Technical Committee on Distributed Processing (TCDP) ; organized by The Hong Kong Polytechnic University, Department of Computing ; symposium general co-chairs: Jiannong Cao (The Hong Kong Polytechnic University, Hong Kong), Michael R. Lyu (The Chinese University of Hong Kong, Hong Kong), 94-103, IEEE, 2017.
2016
DOI	Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. Parameter synthesis for probabilistic systems, MBMV 2016 : 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" : Albert-Ludwigs-Universität Freiburg im Breisgau 1.-2. März 2016 / Ralf Wimmer (Herausgeber), 72-74, Albert-Ludwigs-Universität, 2016.
DOI	Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates, Computer safety, reliability, and security : 35th international conference, SAFECOMP 2016, Trondheim, Norway, September 21-23, 2016 : proceedings / Amund Skavhaug, Jérémie Guiochet, Friedemann Bitsch (eds.), 253-265, Springer, 2016.
2015
DOI	Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. PROPhESY : A PRObabilistic ParamEter SYnthesis Tool, Computer aided verification : 27th international conference, CAV 2015, San Francisco, CA, USA, July 18 - 24, 2015 ; proceedings, part I / Daniel Kroening; Corina S. Păsăreanu (eds.). - Pt. 1, 214-231, Springer International Publishing, 2015.
2014
DOI	Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, Quantitative evaluation of systems : 11th international conference, QEST 2014, Florence, Italy, September 8 - 10, 2014 ; proceedings / Gethin Norman; William Sanders (eds.), 404-420, Springer, 2014.
2013
DOI	Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 21 Seiten, 2013.