Christina Gehnen

Email: christina.gehnen at cs.rwth-aachen.de
Address: Room 4207
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21228

I am a PhD student jointly affiliated with the Software Modeling and Verification Group headed by Professor Joost-Pieter Katoen and the Chair for Quantum Information Systems headed by Professor Dominique Unruh.

Research

My research focuses on deductive verification of quantum programs. In more detail, I work with Quantum Weakest Preconditions, a method to compute the best predicate, that ensures that a given postcondition holds after the quantum program is executed. I consider quantum programs from a theoretical point of view, that means everything I do is based on linear algebra.

Thesis projects

If you are interested in writing a Bachelor’s or Master’s thesis about formal verification of quantum programs, don’t hesitate to contact me.

Past/Current Thesis Projects

Xi Wang: Predicate Transformers for Nondeterministic Quantum Programs (Bachelor Thesis, 2026)
Umut Dural: A Formal Language for Expressing Quantum Predicates (Master Thesis, 2025)
Kaleb Kierner: Modeling Non-deterministic Quantum Programs for Model Checking (Bachelor Thesis, 2025)
Jonas Deutsch: Bounds for Quantum Weakest Preconditions (Master Thesis, 2025)
Felix Faßbender: Explaining Quantum Verification using Automated Quantum Weakest Preconditions (Bachelor Thesis, 2025, co-supervised with Philipp Schroer)

Teaching

WiSe26/27: Probabilistic Programming
SoSe26: Introduction to Quantum Computing (i15)
SoSe26: Seminar Quantum Program Verification (i15)
SoSe25: Introduction to Quantum Computing (i15)
SoSe25: Seminar Quantum Program Logics (i15)
WiSe24/25: Seminar Probabilistic Programming
SoSe24: Introduction to Quantum Computing (i15)

Publications

You can find me on dblp and ORCID.

Peer Review

FM 2024 (external reviewer)
TACAS 2025 (external reviewer)
CAV 2025 (external reviewer)
TACAS 2026 (external reviewer)
POPL 2027 (external reviewer)
Q-STAV 2027 (PC member)

Publications

2025
DOI	Thomas Noll, Christina Gehnen, Roy Hermanns. Quantum Computing: From Weakest Preconditions to Voltage Pulses, Principles of verification: cycling the probabilistic landscape, Part 1 / Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk, editors, 201-229, Springer, 2025.
DOI	Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen. Bayesian Inference in Quantum Programs, 52nd International Colloquium on Automata, Languages, and Programming : ICALP 2025, July 8–11, 2025, Aarhus, Denmark / edited by Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, Gabriele Puppis, 157:1-157:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, 2025.
DOI	Emma Katharina Ahrens, Christina Gehnen, Lena Franziska Verscht. Report on Probability in Computer Science (PICS) 2024, 32-34, ACM, 2025.
2023
DOI	Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, 24, Department of Theoretical Computer Science, Technical University of Braunschweig, 2023.
2022
DOI	Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings / edited by Patricia Bouyer, Lutz Schröder, 449-469, Springer International Publishing, 2022.
DOI	Christina Gehnen. POMDP-based execution models for probabilistic programs with partial observability, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2022.
2021
DOI	Christina Gehnen. Automata-based model checking of recursive systems, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2021.