The CC Chair congratulates Marcus Rossel for receiving the N.-J. Lehmann-Stiftung award for his “outstanding thesis in Computer Science with theoretical focus”. In his thesis, “An Equality Saturation Tactic for Lean”, Marcus built a tactic for the Lean theorem prover that allows mathematicians, computer scientists and others to reason about equations in a much more efficient way. It automates away tasks that can range from tedious to extremely difficult, and lets users focus on the interesting parts of the proof. This work wouldn’t have been possible without the supervision of Andres Goens, a previous PhD student of the CC Chair, who is now a professor in the University of Amsterdam. Marcus is a postgraduate researcher, working on Verified System Design Automation (VerSA) at the Barkhausen Institute in Dresden. He received the award remotely, while attending PLDI’25 in Seoul South Korea, one of top conferences in the field, where he co-authored a paper that used results from his thesis.

We also congratulate Max Kurze for receiving “3m5 award for an outstanding thesis in Computer Science”. Max is currently pursuing a PhD at the Verified System Design Automation (VerSA) group at the Barkhausen Institute in Dresden. In his thesis, “A Framework for Modular and Compositional Formal Reasoning in Koika”, Max devised a novel typed parsing and implemented a Hoare logic reasoning framework, extending Kôika’s semantics to scale provably correct designs towards trustworthy computing systems. This thesis was also supervised by a previous PhD student of the CC Chair, Sebastian Ertel, who leads the VerSA as research group leader at the Barkhausen Institute in Dresden. This is awesome work and we look forward to seeing how Max will build on it during his PhD.