Professor at Saarland University
Lecturer at University College London
I do research in quantitative aspects of formal verification and I am looking for PhD students.
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!
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 programs,
- quantitative aspects of verification in general,
- quantitative aspects of incorrectness logic,
- weighted programming,
- verification of non-functional requirements, e.g. expected runtimes
- machine learning and verification,
- explainable verification,
- recursion theory, and
- (mathematical) logic.
You can find a usually up-to-date list of my publications at dblp and Google Scholar.
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 BACHELOR STUDENTS
- Yannik Schnitzer (as 2nd supervisor)
- 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)
- Sonja Skiba. Towards Completeness of a Proof Rule for Almost-sure Termination. Bacherlor’s thesis @ RWTH Aachen
- David Herzkamp. Hardness of Probabilistic Termination with Nondeterminism. Bachelor’s thesis @ RWTH Aachen
- Joshua Peignier (ENS Rennes). Possibility Distribution Semantics for Probabilistic Programs with Nondeterminism. 2017. Research internship project @ RWTH Aachen (supervision together with Christoph Matheja)
- Sven Deserno, Probabilistic Model Checking for Markov Chain Families. 2017. Master’s thesis @ RWTH Aachen (supervision together with Sebastian Junges)
- Kevin Batz. Proof Rules for Expected Run-Times of Probabilistic Programs. 2017. Bachelor’s thesis @ RWTH Aachen (supervision together with Christoph Matheja)
- Simon Feiden. Extending Probability Generating Function Semantics to Negative Variable Valuations. 2016. Bachelor’s thesis @ RWTH Aachen
- 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.
- 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
- Nomination for Teaching Award at RWTH Aachen 2019
- Nomination for Teaching Award at RWTH Aachen 2015
- Select Attendee of 7th Heidelberg Laureate Forum
- FITWeltweit Scholarship of the DAAD 2016
- CAV 2021 – 33rd Int’l Conf. on Computer-Aided Verification
- CONCUR 2020 – 31st Int’l Conf. on Concurrency Theory, part of QONFEST 2020
- ESOP 2023 – 31st European Symposium on Programming
- ICALP 2022 – 49th Int’l Coll. on Automata, Languages and Programming
- LICS 2022 – 37th Ann. Symp. on Logic in Computer Science, part of FLoC 2022
- LPAR23 – 23rd Int’l Conf. on Logic for Programming, Artificial Intelligence and Reasoning (2020)
- OOPSLA 2022, part of SPLASH 2022
- POPL 2022 – 48th ACM SIGPLAN Symp. on Principles of Programming Languages
- Member of the Committee for Selecting Distinguished Papers
- QEST 2019 – 16th Int’l Conf. on Quantitative Evaluation of SysTems
- QEST 2018 – 15th Int’l Conf. on Quantitative Evaluation of SysTems, part of CONFESTA 2018
- TACAS 2024 – 30th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems
Research Funding Proposals
- 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) (2020)
- Transactions on Computational Logic (TOCL) (2017)
- Transactions on Modeling and Computer Simulation (TOMACS) (2020)
- Transactions on Programming Languages and Systems (TOPLAS) (2019)
I am new here. More content coming soon.