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 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
PEER REVIEW
Conferences:
- 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)