Aller au contenu

Leonardo de Moura

Un article de Wikipédia, l'encyclopédie libre.
Ceci est une version archivée de cette page, en date du 19 novembre 2021 à 18:00 et modifiée en dernier par Cuagga (discuter | contributions). Elle peut contenir des erreurs, des inexactitudes ou des contenus vandalisés non présents dans la version actuelle.
Leonardo de Moura
une illustration sous licence libre serait bienvenue
Biographie
Formation
Activités
Autres informations
A travaillé pour
Amazon Web Services (depuis )
Microsoft Research (-)Voir et modifier les données sur Wikidata
Directeurs de thèse
Carlos José Pereira de Lucena (d), Edward Hermann Haeusler (d)Voir et modifier les données sur Wikidata
Distinction
Œuvres principales
Lean, Z3 Theorem Prover (d)Voir et modifier les données sur Wikidata

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[1].

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[2]. 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[3]. 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[4]. En 2018, son article « Z3: An Efficient SMT Solver » (ETAPS conference) reçoit le Test of time award[5].

Références

  1. (en) « Leonardo de Moura » (consulté le )
  2. (en) « Haifa Verification Conference 2010 » (consulté le )
  3. (en) « Programming Languages Software Award » (consulté le )
  4. « Skolem Award » (consulté le )
  5. (en) « Test of Time Award » (consulté le )

Liens externes