I am looking for Master students!
I do research in quantitative aspects of formal verification. Check out my dplp or Google Scholar to get a feel for my research. More infos coming soon. Feel very welcome to get in touch with me if you are interested!
I am also looking for students who want to do a Bachelor or Master thesis project in logic and/or verification. Do get in touch!
Research
I am interested in quantitative aspects of formal program verification.
To get a feel for my research, you can find my PhD thesis on weakest-precondition-style probabilistic program verification here. It won the Ackermann Award for outstanding dissertations of the European Association for Computer Science Logic (EACSL) in 2020 and I am told that it is quite readable.
More specifically, my research interests include:
- semantics and formal verification of probabilistic and quantum programs
- quantitative aspects of verification in general
- quantitative aspects of incorrectness logic
- non-classical models of computation, e.g. weighted programming
- verification of non-functional requirements, e.g. expected runtimes
- machine learning and verification
- explainable verification
- recursion theory
- (mathematical) logic.
You can find a usually up-to-date list of my publications at dblp and Google Scholar.
Students
I always enjoy working with motivated students with a passion for logic and formal verification. Currently, I am looking for PhD students at Saarland University as well as students who want to do a master’s or bachelor’s thesis project in quantitative aspects of logic and/or verification. Get in touch if you’re interested!
CURRENT PhD STUDENTS
CURRENT UNDERGRADUATE STUDENTS
- Bastian Heinen
- Lucas Kehrer
- Angela Krebs
FORMER STUDENTS (selection)
- Philipp Schröer. A Deductive Verifier for Probabilistic Programs. Master’s Thesis @ RWTH Aachen
- Lena Verscht. Weakest Preexpectation Reasoning for Amortized Expected Runtimes. Bachelor’s Thesis @ RWTH Aachen
- Lutz Klinkenberg. On Probability Generating Functions for Program Analysis. Master’s thesis @ RWTH Aachen
- Kevin Batz. IC3 for Probabilistic Systems. Master’s thesis @ RWTH Aachen (supervision together with Sebastian Junges and Christoph Matheja) and Proof Rules for Expected Run-Times of Probabilistic Programs. Bachelor’s thesis @ RWTH Aachen (supervision together with Christoph Matheja)
- Yannik Schnitzer. On the Robustness of Neural Network Decisions. Bachelor’s Thesis @ UdS (as 2nd supervisor)
- Clara Scherbaum. Probability Generating Function Semantics for Probabilistic Programs. 2016. Bachelor’s thesis @ RWTH Aachen.
Winner of the itestra innovation Award for outstanding bachelor theses.
Awards
RESEARCH
- Distinguished Paper at POPL 2021
- Best Paper Award at LOPSTR 2020
- Ackermann Award for outstanding dissertations 2020
- Nomination for the GI Dissertation Award 2020
- Borchers Badge for doctoral degrees with distinction 2019
- Best Paper Award at SUM 2018
- Nomination for EATCS Best Paper Award at ETAPS (ESOP) 2018
- EATCS Best Paper Award at ETAPS (ESOP) 2016
TEACHING
- Nomination for Teaching Award at RWTH Aachen 2019
- Nomination for Teaching Award at RWTH Aachen 2015
OTHER
- Select Attendee of 7th Heidelberg Laureate Forum
- FITWeltweit Scholarship of the DAAD 2016
Peer Review
Program Committees
- CAV 2024 & 2021 – Int’l Conf. on Computer-Aided Verification
- CONCUR 2024 & 2020 – Int’l Conf. on Concurrency Theory
- CSL 2024 – EACSL Annual Conference on Computer Science Logic
- ESOP 2023 – European Symposium on Programming
- ICALP 2022 – Int’l Coll. on Automata, Languages and Programming
- LAFI 2024 – Workshop on Languages for Inference
- LICS 2022 – Ann. Symp. on Logic in Computer Science
- LPAR 2024 & 2020 – Int’l Conf. on Logic for Programming, Artificial Intelligence and Reasoning
- OOPSLA 2022, part of SPLASH 2022
- POPL 2025 & 2022 – Symp. on Principles of Programming Languages
- Member of the Committee for Selecting Distinguished Papers 2022
- QEST 2023, 2019, 2018 – Int’l Conf. on Quantitative Evaluation of SysTems
- SETTA 2024 – Symp. on Dependable Software Engineering
- TACAS 2024 – Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems
- TPSA 2025 – Workshop on Theory and Practice of Static Analysis
External Reviewer
Research Funding Proposals
Awards
- Best scientific production in Information and Communication Sciences and Technologies in 2022 at the Plateau de Saclay / Université Paris-Saclay, France
Edited Volumes
Journals
- Journal of the ACM (J.ACM) (2023)
- Journal of Logical and Algebraic Methods in Programming (JLAMP) (2022)
- Logical Methods in Computer Science (LMCS) (2022)
- Mathematical Structures in Computer Science (MSCS) (2020)
- Theoretical Computer Science (TCS) (2022 & 2020)
- Transactions on Computational Logic (TOCL) (2017)
- Transactions on Modeling and Computer Simulation (TOMACS) (2020)
- Transactions on Programming Languages and Systems (TOPLAS) (2019)