On Research with Joost-Pieter Katoen

Could you introduce yourself and your research area?

I am Joost-Pieter Katoen, holding the Chair on Software Modeling and Verification at RWTH Aachen, one of the largest technical universities in Germany. I also hold a part-time professorship in the Formal Methods and Tools Group at the University of Twente in my home country The Netherlands. My main research interests lie in concurrency theory, probabilistic computation, formal semantics, model checking, program verification, and software tools. My PhD dissertation (1996) was in the area of “true” concurrency models. Back then, I considered timed and probabilistic extensions of event structures, a semantic model of, for example, process algebras. My interest then shifted to model checking, mostly of probabilistic models such as finite (continuous-time) Markov chains and Markov decision processes. Since about a decade, I got fascinated by probabilistic programming.

I am active in ETAPS since 2002, when I co-chaired TACAS. I am member of the ETAPS SC (almost) since then, and chaired the ETAPS SC 2015-2019. Since 2020, I chair the TACAS SC.

What are the most exciting current advances in your research field?

Our growing understanding of probabilistic programs in all aspects. I mean not only semantic foundations, the essence of probabilistic inference, and (impressive) advances towards automated verification, but also their use in all kinds of interesting application areas. I also find the connection to quantum programs quite exciting.

Let’s talk about that most recent research interest of yours: probabilistic program verification and semantics. What were your reasons to go into this direction in the first place and how did you go about gaining foothold in this field?

I was reading the seminal book by Annabelle McIver and Carroll Morgan on weakest-precondition reasoning (wp-reasoning) of probabilistic programs, and I found the leap from finite Markov models to such symbolic representations of infinite-state models quite appealing. After visiting them in 2009—the field of probabilistic programming was still in its infancy—, co-supervising a PhD student, and writing some joint papers, I got more and more acquainted with their way of reasoning and the strengths of (and possibilities to improve) wp-reasoning. We invested quite a bit in giving an operational interpretation of their wp-reasoning, which to me was an important step for a better understanding.

During these years, probabilistic programming emerged, and we started contributing to first workshops on the topic (now emerged into LAFI), and later—once the topic was generally adopted—to major programming language conferences in the field such as POPL, OOPSLA, and ESOP. For me this was a shift from my “home” conferences—such as CONCUR, TACAS, and CAV—towards programming languages. Honestly, I got confronted with wp-calculi when I spent two years at the TU Eindhoven after my master’s and found it pretty abstract. I never expected to work on these things myself.

But may I ask: Given that wp seemed to be out of your comfort zone, why did that not deter you from continuing to work on it?

I really wanted to understand the ins and outs of wp-reasoning. The idea was to consider possibilities on partial automation of the approach. This led to some first ideas on loop-invariant synthesis. Though we had this paper at SAS 2010, I felt that an operational interpretation would be very helpful to better grasp what weakest pre-conditions on probabilistic programs really are. This curiosity-driven research has—retrospectively—been quite successfully although even after more than a decade I have more questions than answers.

I firmly believe that rather than finding ways to extend the research result in your last paper to “produce” a next paper, one should focus more on research questions that really matter to you and that you are curious about.

What do you expect will be the next big thing/challenge in this field?

Probabilistic programming in a concurrent setting. Quantum programming, too.

What advice would you give to someone just starting their carreer in research?

Go outside of your comfort zone. I spent two years after my studies in Eindhoven with Martin Rem—one of the (only) four PhD students who graduated with Dijkstra—where I learnt the ins and outs of Dijkstra’s correct-by-design programming paradigm. This was an eye-opener. I spent my postdoc in Erlangen with Ulrich Herzog, an expert on performance analysis and queueing theory. This was fascinating for me and an extremely fruitful experience. He gave me the chance to develop my own course. Do something new, he said. That’s how I got into model checking. During my work on probabilistic model checking, I worked together with experts in performance and dependability analysis. This all broadened my scope considerably.

Finally, who would you like to see interviewed on the ETAPS blog?

Supratik Chakraborty (IIT Mumbai).

And which paper would you recommend everyone to read?

That’s a difficult one. Let me mention a paper that I consider as a true breakthrough in concurrency:

Kenneth L. McMillan. A Technique of State Space Search Based on Unfolding. Formal Methods Syst. Des. 6(1): 45-65 (1995)

It is based on Ken’s 1992 CAV paper. A must-read (and must-teach) in concurrency theory!