Hannah Mertens
- hannah.mertens at cs.rwth-aachen.de
- Address
- Room 4207
Ahornstraße 55
D-52074 Aachen - Phone
- +49 241 80 21203
I am a PhD student in the Software Modeling and Verification Group headed by Professor Joost-Pieter Katoen.
Research
My research focuses on compositional verification of probabilistic systems, in particular parametric Markov models and stochastic games.
Teaching
Current semester
Past semesters
- SoSe25: Formale Systeme, Automaten, Prozesse
- WiSe24/25: Model Checking and Seminar Trends in Computer-Aided Verification
- SoSe24: Formale Systeme, Automaten, Prozesse
- WiSe23/24: Seminar Reproducing Research Results in Formal Methods
- SoSe23: Datenstrukturen und Algorithmen
Thesis projects
If you are interested in writing a Bachelor’s or Master’s thesis in probabilistic model checking, don’t hesitate to contact me.
Ongoing Thesis Projects
- Sophia Schweizer, Interval MDP Semantics for Multi-Objective Properties. Bachelor’s thesis
- Jesper Nilsson, Expected Visiting Times in Interval Markov Chains. Bachelor’s thesis
- Toufik Kairoua, Weakest-preconditions for Interval-Programs. Bachelor’s thesis(co-supervision with Lena Verscht)
- Svenja Stein, AG-Reasoning for poMDPs (working title). Master’s thesis (co-supervision with Alexander Bork)
Past Thesis Projects
- Sven Farwig, An Evaluation of Tools to Compute the Stationary Distribution in Markov Chains. Bachelor’s thesis
- Asad Butt, Extending AG-Rules for pPAs. Bachelor’s thesis
- Julian Bahr, Properties and Complexity of Cores in Markov Chains. Bachelor’s thesis (co-supervision with Tim Quatmann)
- Marcel Eissing, On the Relation of Rely-Guarantee and Assume-Guarantee Reasoning. Bachelor’s thesis (co-supervision with Lena Verscht)
- Jannik Hiller, Model Checking Stochastic Games with Storm. Bachelor’s thesis (co-supervision with Tim Quatmann)
- Julius Ide, Markov Decision Processes with Multiple Linear Time and Long-run Average Objectives. Bachelor’s thesis (co-supervision with Tim Quatmann)
Awards
- ETAPS2024: Our paper Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains (joint work with Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler) has received the EAPLS (European Association of Programming Languages) Best Paper Award.
- Springorum Medal in 2023 for receiving a master’s degree with distinction.
Publications
Publications
| 2025 | |
|---|---|
| DOI | Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler. Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate, 23, Springer Science + Business Media B.V., 2025. |
| DOI | Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen. Compositional Reasoning for Parametric Probabilistic Automata, 36th international conference on concurrency theory : CONCUR 2025, august 26-29, 2025, aarhus, denmark / edited by patricia bouyer, jaco van de pol, 31:1-31:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, 2025. |
| DOI | Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen. Compositional Reasoning for Parametric Probabilistic Automata, 2025. |
| 2024 | |
| DOI | Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains, Tools and algorithms for the construction and analysis of systems / bernd finkbeiner, laura kovács, editors. - Part 2, 237-257, Springer, 2024. |