Leonardo de Moura
# Leonardo de Moura

Leonardo Mendonça de Moura est un informaticien brésilien, chercheur chez Microsoft Research et l'auteur des assistants de preuve Z3 (en) et Lean.

## Formation et carrière

Leonardo de Moura obtient son doctorat à l'université pontificale catholique de Rio de Janeiro en 2000. En 2006, il intègre Microsoft Research où il devient Senior Principal Researcher du groupe RiSE.

## Prix et distinctions

Il est lauréat avec Nikolaj Bjørner du prix Herbrand en 2019 « pour ses nombreuses et importantes contributions à la résolution de problèmes SMT, dont sa théorie, son implémentation et son application à une large gamme de besoins universitaires et industriels ». Auparavant il a reçu en 2010 le Haifa Verification Conference Award. En 2014, son article Z3: An Efficient SMT Solver (TACAS conference) reçoit le prix du The most influential tool paper in the first 20 years of TACAS. Son logiciel assistant de preuve Z3 (en) reçoit en 2015 le Programming Languages Software Award. En 2017 il est lauréat avec Nikolaj Bjørner du prix Skolem pour son article « Efficient E-Matching for SMT Solvers » qui a résisté à l'épreuve du temps, en étant un des articles les plus influents dans le domaine. En 2018, son article « Z3: An Efficient SMT Solver » (ETAPS conference) reçoit le Test of time award.

