On the ETAPS 2025 Dissertation Award

Kevin Batz has had a busy start of the year. He finished his PhD thesis at the RWTH Aachen University, supervised by Joost-Pieter Katoen, then moved to London to start a postdoc position at UCL, and flew to Hamilton to join ETAPS and receive this year’s ETAPS dissertation award.

Kevin, first things first: Congratulations! Can you tell us when and where you heard about winning this award?

Thank you! It was one of my first days as a postdoc at University College London, and I was waiting outside the secretary’s office to sort out some contractual matters when I saw the email on my phone. I was—and still am—so happy!

Let’s talk about your thesis. What is it all about?

My thesis is about verifying probabilistic programs, which are ordinary programs that have access to a source of randomness. Applications include the implementation of randomized algorithms, modeling systems that operate in uncertain environments, and machine learning.

Verifying probabilistic programs involves answering questions like: “Is the probability of terminating in a given error state sufficiently small?” Manual reasoning about such quantitative properties is, however, difficult and error-prone. We need computer-aided techniques to support us. Towards this end, my thesis contributes both foundational aspects of the deductive (i.e., Hoare logic-like) verification of probabilistic programs and novel algorithms.

Foundational aspects include a probabilistic assertion language for specifying properties of interest in a principled way, which has paved the way for the development of CAESAR, an automated deductive verifier for probabilistic programs. On the more algorithmical side, my thesis includes techniques for automating invariant-based reasoning through novel induction principles and loop invariant generators that enable the fully automatic verification of infinite-state probabilistic programs with loops.

Did you know that you wanted to write your thesis about verifying probabilistic programs?

Yeah, I knew that I wanted to work on verifying probabilistic programs deductively, as deductive program verification has fascinated me ever since my first year at university. Through a job as a student assistant at Joost-Pieter Katoen’s chair, I had the opportunity to get a taste of the field already before starting my PhD. During my PhD, I realized that it is important to learn identifying relevant and open problems within the respective field of research. The specific topics of my thesis emerged only later, inspired by talks, papers, and conversations with other researchers.

Is there any open problem related to your thesis you really would like to solve?

For sure! In my thesis, I present an expressive quantitative assertion language for probabilistic weakest preconditions. Intuitively, expressivity means that the assertion language includes all loop invariants required for verifying probabilistic programs. This result applies to all programs that manipulate numeric program variables. I conjecture that it also extends to probabilistic pointer programs (i.e., probabilistic programs that manipulate dynamic memory) and to a probabilistic extension of separation logic. However, it is just a conjecture…

Besides your research, what were some of the highlights of your PhD?

A recurring highlight of my time as a PhD student was the many research trips and conferences I attended. I truly enjoyed meeting and working with researchers from all over the world, which greatly broadened both my academic and personal horizons. I also enjoyed interactions with undergrad students a lot: Whether it was spontaneous discussions on proof strategies during exercise classes or meetings with students working on their theses, I always looked forward to hearing their interesting questions and sometimes brilliant insights.

You are now a postdoctoral researcher at UCL London, working with Alexandra Silva. What are you working on and how does this relate to your previous work?

We are working on the verification of packet-switched computer networks. While my expertise in verifying probabilistic systems is useful when it comes to reasoning about, e.g., faulty networks or randomized routing algorithms, network verification also involves reasoning about quantitative properties beyond probabilistic ones. This is really exciting, as I am exposed to many new challenges and open problems that we need to tackle to make the verification of computer networks feasible.

Thanks, Kevin! Will we see you at ETAPS next year?

It helps if I get a paper in, but I will certainly try! In fact, I’ve been to ETAPS already four times. I particularly enjoy the wide range of topics covered across the various conferences and workshops. Beyond the technical content, it’s simply a great community—people are kind, curious, and always up for a good conversation or a nice drink.