Lena Verscht
lverscht at cs.uni-saarland.de
Saarland Informatics Campus
E1 3, R. 507
66133 Saarbrücken
I am a PhD student in the Software Modeling and Verification Group at RWTH Aachen headed by Professor Joost-Pieter Katoen and in the Quantitative Verification Group at Saarland University headed by Professor Benjamin Kaminski.
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:
- Marcel Eissing. Bachelor’s thesis
- Angela Krebs. Existential Logic: A New Perspective on Identifying Bugs. Bachelor’s thesis
Past thesis projects:
- 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:
- Introduction to Program Analysis @RWTH (Proseminar, Summer 2025)
Past semesters:
- 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
PEER REVIEW
Conferences:
- 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)