Matthias Volk

dav
Email
Click to reveal
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:

Teaching

I am currently involved in the following teaching activities:

Past teaching activities:

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.

2022
DOI fulltext PDF [bibtex]
@article{D2022,
title = {DFT modeling approach for operational risk assessment of railway infrastructure},
author = {Norman Weik and Matthias Volk and Joost-Pieter Katoen and Nils Nießen},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {24(3)},
pages = {pages 331-350},
type = {Journal Article},
year = {2022},
doi = {10.1007/s10009-022-00652-4},
url = { https://publications.rwth-aachen.de/record/844073},
}×
[issue]
Norman Weik, Matthias Volk, Joost-Pieter Katoen, Nils Nießen. DFT modeling approach for operational risk assessment of railway infrastructure, International journal on software tools for technology transfer 24 (3), pages 331-350, Springer, 2022.
DOI [bibtex]
@conference{BSBEASDFT2022,
title = {BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees},
author = {Daniel Basgöze and Matthias Volk and Joost-Pieter Katoen and Shahid Khan and Marielle Stoelinga},
publisher = {Springer},
booktitle = {LNCS},
volume = {13260},
pages = {713-732},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-06773-0_38},
url = { https://publications.rwth-aachen.de/record/951563},
}×
[issue]
Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, Marielle Stoelinga. BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees, 14. International Symposium NASA Formal Methods (NFM 2022), Volume 13260 of LNCS, 713-732, Springer, 2022.
DOI fulltext PDF [bibtex]
@phdthesis{D2022,
title = {Dynamic fault trees: semantics, analysis and applications},
author = {Matthias Volk},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {PhD Thesis},
year = {2022},
doi = {10.18154/RWTH-2023-04092},
url = { https://publications.rwth-aachen.de/record/956330},
}×
[issue]
Matthias Volk. Dynamic fault trees: semantics, analysis and applications, PhD Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2022.
2021
DOI fulltext PDF [bibtex]
@article{TS2021,
title = {The probabilistic model checker STORM},
author = {Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {24(4)},
pages = {pages 589-610},
type = {Journal Article},
year = {2021},
doi = {10.1007/s10009-021-00633-z},
url = { https://publications.rwth-aachen.de/record/822059},
}×
[issue]
Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. The probabilistic model checker STORM, International journal on software tools for technology transfer 24 (4), pages 589-610, Springer, 2021.
DOI [bibtex]
@conference{MCMFLF2021,
title = {Model Checking the Multi-Formalism Language FIGARO},
author = {Shahid Khan and Matthias Volk and Joost-Pieter Katoen and Alexis Braibant and Marc Bouissou},
publisher = {IEEE},
pages = {463-470},
type = {Conference Paper},
year = {2021},
doi = {10.1109/DSN48987.2021.00056},
url = { https://publications.rwth-aachen.de/record/835145},
}×
[issue]
Shahid Khan, Matthias Volk, Joost-Pieter Katoen, Alexis Braibant, Marc Bouissou. Model Checking the Multi-Formalism Language FIGARO, 51. Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 463-470, IEEE, 2021.
DOI fulltext PDF [bibtex]
@article{S2021,
title = {Synthesizing optimal bias in randomized self-stabilization},
author = {Matthias Volk and Borzoo Bonakdarpour and Joost-Pieter Katoen and Saba Aflaki},
publisher = {Springer},
journal = {Distributed computing},
volume = {35(1)},
pages = {pages 37-57},
type = {Journal Article},
year = {2021},
doi = {10.1007/s00446-021-00408-4},
url = { https://publications.rwth-aachen.de/record/835189},
}×
[issue]
Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Saba Aflaki. Synthesizing optimal bias in randomized self-stabilization, Distributed computing 35 (1), pages 37-57, Springer, 2021.
DOI [bibtex]
@conference{MAFSVDFT2021,
title = {Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees},
author = {Shahid Khan and Joost-Pieter Katoen and Matthias Volk and Ahmad Zafar and Falak Sher},
publisher = {IEEE},
type = {Conference Paper},
year = {2021},
doi = {10.1109/LADC53747.2021.9672579},
url = { https://publications.rwth-aachen.de/record/841297},
}×
[issue]
Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Ahmad Zafar, Falak Sher. Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees, 10. Latin-American Symposium on Dependable Computing (LADC), IEEE, 2021.
DOI [bibtex]
@conference{SRALV2021,
title = {Scalable Reliability Analysis by Lazy Verification},
author = {Shahid Khan and Joost-Pieter Katoen and Matthias Volk and Marc Bouissou},
publisher = {Springer},
booktitle = {LNCS},
volume = {12673, Programming and software engineering},
pages = {180-197},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-76384-8_12},
url = { https://publications.rwth-aachen.de/record/841298},
}×
[issue]
Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Marc Bouissou. Scalable Reliability Analysis by Lazy Verification, 13. NASA Formal Methods Symposium (NFM 2021), Volume 12673, Programming and software engineering of LNCS, 180-197, Springer, 2021.
2020
fulltext PDF [bibtex]
@techreport{URTGURAVL2020,
title = {UnRAVeL Research Training Group: Uncertainty and Randomness in Algorithms, Verification, and Logic},
author = {Joost-Pieter Katoen and Martin Ritzert and Richard Marlon Wilke and Katrin M. Dannert and Peter Lindner and Dennis Fischer and Janosch Fuchs and Björn Frederik Tauer and Vipin Ravindran Vijayalakshmi and Laura Vargas Koch and Nadine Friesen and Andreas Gabriel Klinger and Marcel Tobias Hark and Benjamin Lucien Kaminski and Sebastian Junges and Jip Josephine Spel and Anton Pirogov and Stefan Schupp and Till Hofmann and Daxin Liu and Martin Comis and Tabea Claudia Krabs and Stephan Zieger and Rebecca Haehn and Matthias Volk and Norman Weik and Helene-Maria Bolke-Hermanns},
pages = {85 Seiten},
type = {Tech Report},
year = {2020},
url = { https://publications.rwth-aachen.de/record/807487},
}×
[issue]
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 [bibtex]
@article{S2019,
title = {Safety analysis for vehicle guidance systems with dynamic fault trees},
author = {Majdi Ghadhab and Sebastian Junges and Joost-Pieter Katoen and Matthias Kuntz and Matthias Volk},
publisher = {Elsevier Science},
journal = {Reliability engineering & system safety},
volume = {186},
pages = {pages 37-50},
type = {Journal Article},
year = {2019},
doi = {10.1016/j.ress.2019.02.005},
url = { https://publications.rwth-aachen.de/record/755407},
}×
[issue]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Safety analysis for vehicle guidance systems with dynamic fault trees, Reliability engineering & system safety 186, pages 37-50, Elsevier Science, 2019.
DOI [bibtex]
@conference{ADMAIRARSA2019,
title = {A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas},
author = {Matthias Volk and Norman Weik and Joost-Pieter Katoen and Nils Nießen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11687},
pages = {40-58},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-27008-7_3},
url = { https://publications.rwth-aachen.de/record/766655},
}×
[issue]
Matthias Volk, Norman Weik, Joost-Pieter Katoen, Nils Nießen. A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas, 24. International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019), Volume 11687 of LNCS, 40-58, Springer, 2019.
DOI [bibtex]
@conference{FVRRDFT2019,
title = {Formal Verification of Rewriting Rules for Dynamic Fault Trees},
author = {Yassmeen Elderhalli and Matthias Volk and Osman Hasan and Joost-Pieter Katoen and Sofiène Tahar},
publisher = {Springer},
booktitle = {LNCS},
volume = {11724, Theoretical computer science and general issues},
pages = {513-531},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-30446-1_27},
url = { https://publications.rwth-aachen.de/record/766660},
}×
[issue]
Yassmeen Elderhalli, Matthias Volk, Osman Hasan, Joost-Pieter Katoen, Sofiène Tahar. Formal Verification of Rewriting Rules for Dynamic Fault Trees, 17. edition of the International Conference on Software Engineering and Formal Methods (SEFM 2019), Volume 11724, Theoretical computer science and general issues of LNCS, 513-531, Springer, 2019.
DOI [bibtex]
@conference{SRMLBRD2019,
title = {Synergizing Reliability Modeling Languages: BDMPs without Repairs and DFTs},
author = {Shahid Khan and Joost-Pieter Katoen and Matthias Volk and Marc Bouissou},
publisher = {IEEE},
pages = {266-275},
type = {Conference Paper},
year = {2019},
doi = {10.1109/PRDC47002.2019.00057},
url = { https://publications.rwth-aachen.de/record/786900},
}×
[issue]
Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Marc Bouissou. Synergizing Reliability Modeling Languages: BDMPs without Repairs and DFTs, 24. Pacific Rim International Symposium on Dependable Computing (PRDC), 266-275, IEEE, 2019.
2018
DOI [bibtex]
@article{FDFTAMCT2018,
title = {Fast Dynamic Fault Tree Analysis by Model Checking Techniques},
author = {Matthias Volk and Sebastian Junges and Joost-Pieter Katoen},
publisher = {IEEE},
journal = {IEEE transactions on industrial informatics},
volume = {14(1)},
pages = {pages 370-379},
type = {Journal Article},
year = {2018},
doi = {10.1109/TII.2017.2710316},
url = { https://publications.rwth-aachen.de/record/713138},
}×
[issue]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques, IEEE transactions on industrial informatics 14 (1), pages 370-379, IEEE, 2018.
DOI [bibtex]
@conference{ONFAAUSDFTUG2018,
title = {One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs},
author = {Sebastian Junges and Joost-Pieter Katoen and Marielle Stoelinga and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10877},
pages = {272-293},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-91268-4_14},
url = { https://publications.rwth-aachen.de/record/753065},
}×
[issue]
Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk. One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs, 39. International Conference on Applications and Theory of Petri Nets and Concurrency (PETRI NETS 2018), Volume 10877 of LNCS, 272-293, Springer, 2018.
2017
arXiv:1702.04311 [bibtex]
@unpublished{ACAMPMC2017,
title = {A storm is Coming: A Modern Probabilistic Model Checker},
author = {Hans Christian Dehnert and Sebastian Junges and Joost-Pieter Katoen and Matthias Volk},
pages = {14 Seiten : Tabellen, Diagramme},
type = {Preprint},
year = {2017},
url = { https://arxiv.org/abs/1702.04311},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A storm is Coming: A Modern Probabilistic Model Checker, 14 Seiten : Tabellen, Diagramme, 2017. https://arxiv.org/abs/1702.04311
DOI [bibtex]
@conference{ASCAMPMC2017,
title = {A Storm is Coming: A Modern Probabilistic Model Checker},
author = {Hans Christian Dehnert and Sebastian Junges and Joost-Pieter Katoen and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10427},
pages = {592-600},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-63390-9_31},
url = { https://publications.rwth-aachen.de/record/713569},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker, 29. International Conference on Computer-Aided Verification (CAV 2017), Volume 10427 of LNCS, 592-600, Springer, 2017.
DOI [bibtex]
@conference{MSAVGS2017,
title = {Model-based Safety Analysis for Vehicle Guidance Systems},
author = {Majdi Ghadhab and Sebastian Junges and Joost-Pieter Katoen and Matthias Kuntz and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10488},
pages = {3-19},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-66266-4_1},
url = { https://publications.rwth-aachen.de/record/713577},
}×
[issue]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems, 36. International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2017), Volume 10488 of LNCS, 3-19, Springer, 2017.
DOI [bibtex]
@conference{AFTPSSA2017,
title = {Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms},
author = {Saba Aflaki and Matthias Volk and Borzoo Bonakdarpour and Joost-Pieter Katoen and Arne Storjohann},
publisher = {IEEE},
pages = {94-103},
type = {Conference Paper},
year = {2017},
doi = {10.1109/SRDS.2017.22},
url = { https://publications.rwth-aachen.de/record/713578},
}×
[issue]
Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Arne Storjohann. Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms, 36. International Symposium on Reliable Distributed Systems (SRDS 2017), 94-103, IEEE, 2017.
2016
DOI fulltext PDF [bibtex]
@conference{P2016,
title = {Parameter synthesis for probabilistic systems},
author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Albert-Ludwigs-Universität},
pages = {72-74},
type = {Conference Paper},
year = {2016},
doi = {10.6094/UNIFR/10639},
url = { https://publications.rwth-aachen.de/record/683021},
}×
[issue]
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, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), 72-74, Albert-Ludwigs-Universität, 2016.
DOI [bibtex]
@conference{ADFTAGSSSFSFR2016,
title = {Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates},
author = {Matthias Volk and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9922},
pages = {253-265},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-45477-1_20},
url = { https://publications.rwth-aachen.de/record/684646},
}×
[issue]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates, 35. International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Volume 9922 of LNCS, 253-265, Springer, 2016.
2015
DOI [bibtex]
@conference{PAPPST2015,
title = {PROPhESY: A PRObabilistic ParamEter SYnthesis Tool},
author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {9206},
pages = {214-231},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-21690-4_13},
url = { https://publications.rwth-aachen.de/record/564236},
}×
[issue]
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, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, 214-231, Springer, 2015.
2014
DOI [bibtex]
@conference{APPV2014,
title = {Accelerating Parametric Probabilistic Verification},
author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {8657},
pages = {404-420},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-10696-0_31},
url = { https://publications.rwth-aachen.de/record/540007},
}×
[issue]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 11. International Conference on Quantitative Evaluation of Systems (QEST 2014), Volume 8657 of LNCS, 404-420, Springer, 2014.
2013
arXiv:1312.3979 [bibtex]
@unpublished{APPV2013,
title = {Accelerating Parametric Probabilistic Verification},
author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
pages = {21 Seiten},
type = {Preprint},
year = {2013},
url = { https://arxiv.org/abs/1312.3979},
}×
[issue]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 21 Seiten, 2013. https://arxiv.org/abs/1312.3979