I am a PhD student jointly affiliated with the Chair for Quantum Information Systems and the Software Modeling and Verification Group (MOVES) at RWTH Aachen.
Contact
Email: christina.gehnen at cs.rwth-aachen.de
Phone: +49 241 80 21228
Campus Boulevard 55–57 Building 4731 52074 Aachen
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. It would be good if you have some basic knowledge about quantum computing and/or program logics (e.g. from taking the ‘Introduction to Quantum Computing’ or ‘Probabilistic Programming’ lecture).
Current / Past 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
- SoSe26: Introduction to Quantum Computing
- SoSe26: Seminar - Quantum Program Verification
- SoSe25: Introduction to Quantum Computing
- SoSe25: Seminar - Quantum Program Logics
- WiSe24/25: Seminar - Probabilistic Programming (i2)
- SoSe24: Introduction to Quantum Computing