I am looking for PhD students!

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!

---

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 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.

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

• Linpeng Zhang

CURRENT BACHELOR STUDENTS

• Yannik Schnitzer (as 2nd supervisor)

FORMER STUDENTS

• 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.

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 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

External Reviewer

Research Funding Proposals

• Israel Science Foundation (ISF) (2022)
• Czech Science Foundation (GACR) (2019)

Edited Volumes

• Foundations of Programming and Software Systems – Probabilistic Programming (2019)

Journals

• 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)

Conferences

---

I am new here. More content coming soon.