Programming Languages and Verification

Jun.-Prof. Dr. Kevin Batz

Research

Our research lies at the intersection of verification, automated reasoning, and mathematical logic. We develop logics and methods for verifying and synthesizing probabilistic and, more generally, quantitative systems, with a particular focus on parametric and infinite-state systems. A central question is how far reasoning about their behavior can be automated, even when it involves uncertainty or nondeterminism.

To this end, we use quantitative program logics, automated proof search, satisfiability modulo theories (SMT), synthesis, and active learning. We also use interactive theorem provers such as Lean 4 to formalize and check the mathematical arguments underlying these methods.

Our research combines theoretical foundations with the development of practical software tools. We aim to turn semantic concepts into methods that analyze complex systems, establish their correctness, or automatically construct systems with desired properties. Applications range from proving the correctness of randomized algorithms to investigating the reliability of computer networks or data center network topologies under uncertainty.