Jasmin Blanchette

Jasmin Blanchette is a Professor of Theoretical Computer Science and Theorem Proving at the Institute for Informatics, Ludwig-Maximilians-Universität München (LMU), where he also serves as Dean of Studies for Computer Science since January 2024. He is additionally affiliated as a guest researcher with the VeriDis group at Loria in Nancy, France.

His research lies at the intersection of automated and interactive theorem proving, with a focus on higher-order logic and proof automation. Key projects include the development of tools like Sledgehammer, Nitpick, and Zipperposition, and foundational work on (co)datatypes and higher-order superposition.

His recent publications reflect a strong trend in formalizing and verifying automated reasoning techniques, especially in higher-order logic, with applications in proof automation, SMT solving, and logical verification. Articles frequently appear in top venues such as CADE, ITP, and the Journal of Automated Reasoning.

• CADE 2023 Best Paper Award for 'Verified given clause procedures'
• FroCoS 2023 Best Paper Award (with Visa Nummelin and Sander Dahmen)
• IPA Dissertation Award (awarded to his student Petar Vukmirović)
• Dutch 'cum laude' distinction (awarded to his student Anne Baanen)
• Dutch Prize for ICT Research 2022

Blanchette has advised numerous PhD and postdoctoral researchers, many of whom are now active contributors to the formal methods community. He has received significant research grants through projects like Matryoshka and Nekoka. He is also the editor-in-chief of the Journal of Automated Reasoning and plays a central role in organizing key conferences such as ITP, CADE, and CPP.

He leads an active research group at LMU, consisting of postdocs and PhD students working on topics such as higher-order superposition, formalization of voting systems, categorical logic, and proof search heuristics. The team collaborates closely with international groups, including those at Inria and TU Wien.