Two BI Researchers Receive Awards for Outstanding Theses
We are delighted to announce that Max Kurze and Marcus Rossel, researchers at the Barkhausen Institut, have been honored with awards for their exceptional diploma and master theses respectively in Computer Science.
Max Kurze Wins 3m5 Thesis Award
Max Kurze received 1,500 EUR from 3m5 for his thesis “A Framework for Modular and Compositional Reasoning in Kôika”, achieving a final grade of 1.0, supervised by Dr.-Ing Sebastian Ertel from Barkhausen Institut, Dresden. Max’s research work advances formal verification in hardware design—a key field for digital sovereignty and trustworthy chip development.
His thesis extended the Kôika language to support complex reasoning tasks, including typed parsing and a Hoare logic. Notably, he reestablished the correctness of Kôika’s compiler after modifying its semantics—an achievement usually expected at the PhD level. His implementation in the Rocq Prover is technically strong and ready for further research.
Marcus Rossel Receives N.-J. Lehmann Foundation Award
Marcus Rossel was awarded 2,000 EUR by the N.-J. Lehmann Foundation for his thesis “An Equality Saturation Tactic for Lean”, also graded 1.0. He developed a tactic that automates equational reasoning in the Lean theorem prover, reducing complexity for users and enabling more efficient proofs.
His work, based on research presented at POPL, required a deep understanding of equality saturation, type theory, and Lean’s metaprogramming framework. Marcus also introduced features like conditional rewriting and type class support, making the tactic highly practical for the Lean community.
We warmly congratulate both awardees and look forward to their continued contributions to trustworthy and future-oriented computing!