Hannah Mertens

Email

hannah.mertens@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

• Seminar Trends in Computer-Aided Verifiaction

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

All records on RWTH Publications