Lena Verscht

Email

lena.verscht at cs.rwth-aachen.de

Address

Room 4207
Ahornstraße 55
D-52074 Aachen

Phone

+49 241 80 21224

I am a PhD student in the Quantitative Verification Group at Saarland University headed by Professor Benjamin Kaminski and in the Software Modeling and Verification Group at RWTH Aachen headed by Professor Joost-Pieter Katoen.

Research

My research interests include the deductive verification of probabilistic programs, as well as quantitative aspects of (partial) incorrectness logic. I am also interested in the connection between Hoare logic and Kleene algebra. Currently, I am studying the precise relationship and expressiveness of both approaches.

Thesis projects

If you are interested in writing a Bachelor’s or Master’s thesis in quantitative aspects of logic or verification, don’t hesitate to contact me. For an overview of currently available topics, see our thesis projects. I am currently supervising the following students:

• Toufik Kairoua. Bachelor’s thesis (joint supervision with Hannah Mertens)
• Anike Heikrodt. Master’s thesis
• Johanna Schneider. Hoare-Like Logics: An Abstract Interpretation Perspective. Bachelor’s thesis

Past thesis projects:

• Marcel Eissing. On the Relation of Rely-Guarantee and Assume-Guarantee Reasoning. Bachelor’s thesis (joint supervision with Hannah Mertens).
• Angela Krebs. Existential Logic: A New Perspective on Identifying Bugs. Bachelor’s thesis
• Anran Wang. Necessary Liberal Preconditions: A Proof System. Master’s thesis
• Haya Alkhaled. A Strongest-Post-Style Calculus for Reasoning about Runtimes. Bachelor’s thesis

Teaching

I am currently involved in the following teaching activities:

• Fixed Point Theory @UdS (Seminar, Summer 2026)

Past semesters:

• Model Checking @RWTH (Lecture, Winter 2025)
• Introduction to Program Analysis @RWTH (Proseminar, Summer 2025)
• Probabilistic Programming @RWTH (Seminar, Winter 2024)
• Probabilistic Programming @RWTH (Lecture, Summer 2024)
• Datenstrukturen und Algorithmen @RWTH (Proseminar, Summer 2024)
• Aspects of Quantitative Program Verification @UdS (Seminar, Winter 2023)
• Program Analysis @UdS (Lecture, Winter 2023)
• Aspects of Quantitative Program Verification @UdS (Seminar, Summer 2023)

Publications

• Lena Verscht, Anrán Wáng, and Benjamin Lucien Kaminski. Partial Incorrectness Logic, arXiv preprint of extended abstract presented at the workshop on Theory and Practice of Static Analysis at POPL 2025
• Lena Verscht and Benjamin Lucien Kaminski. A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests, Proceedings of the ACM on programming languages 9 (POPL), ACM, 2025
• Lena Verscht and Benjamin Lucien Kaminski. Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic, Incorrectness Logic, and Beyond, arXiv preprint of extended abstract presented at the workshop on Formal Methods for Incorrectness 2024 at POPL 2024
• Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht. A Calculus for Amortized Expected Runtimes, Proceedings of the ACM on programming languages 7 (POPL), ACM, 2023

Community service

Peer review:

• ICALP 2026 (External Reviewer)
• PLDI 2026 (External Reviewer)
• LICS 2026 (External Reviewer)
• CAV 2025 (External Reviewer)
• POPL 2025 (External Reviewer)
• LPAR 2024 (External Reviewer)
• CAV 2024 (External Reviewer)
• TACAS 2024 (Member of Artifact Evaluation Committee)
• CSL 2024 (External Reviewer)
• QEST 2023 (External Reviewer)

System administration:

• LICS 2026
• ATVA 2026

Publications