Dr. Jasmin Christian Blanchette

Senior Guest Researcher


Max-Planck-Institut für Informatik

Campus E1 4, Building E1 5, Room 621

66123 Saarbrücken

Physical Address: Building E1 5, room 621

Phone: +49 (0)681 9325 2915

Fax: +49 (0)681 9325 2999

Email: jasmin.blanchette@mpi-inf.mpg.de

Home page: people.mpi-inf.mpg.de/~jblanche

Personal Information

I am a researcher in the VeriDis group at Inria Nancy – Grand-Est and LORIA in Nancy, France, and a senior guest researcher in the Automation of Logic group at the Max Planck Institute for Informatics in Saarbrücken, Germany. Until the end of 2014, I was a postdoc at the Chair for Logic and Verification at the Technische Universität München, Germany, which I joined in 2008 as a Ph.D. student. From 2000 to 2008, I worked as software engineer and documentation manager for Trolltech (now The Qt Company) in Oslo, Norway.

My research focuses on the use of first-order automatic theorem provers and model finders to find proofs and counterexamples in higher-order logic (Sledgehammer, Nitpick, and Nunchaku). Another aspect of my work is the development of foundational definitional mechanisms for (co)datatypes and (co)recursive functions. I am also interested in formalizing classic results and modern research in automated reasoning (IsaFoL).

See my home page for details.