Christina Gehnen
- 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
- 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
- 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.
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. |