Kevin Batz · PostDoc · Cornell University

My work is in verification, automated reasoning, and logic. I develop methods for verifying and synthesizing probabilistic and, more generally, quantitative systems, especially when they are infinite-state or parametric. A central question for me is how much of this reasoning can be automated.

I use quantitative program logics, proof search, synthesis, and active learning. I also use theorem provers, including Lean, to formalize and check the mathematical arguments behind these methods. A recurring theme is to connect semantic ideas with usable verification techniques for probabilistic programs, quantitative networks, and systems whose behavior involves uncertainty, nondeterminism, or parameters.

I am a postdoc at Cornell University, working with Alexandra Silva. I received my PhD summa cum laude (with distinction) from RWTH Aachen University in December 2024, advised by Joost-Pieter Katoen. My dissertation, Automated Deductive Verification of Probabilistic Programs, received the ETAPS Doctoral Dissertation Award in 2025.

Starting in September 2026, I will join the University of Münster as Juniorprofessor of Computer Science.