Leonardo de Moura

Page d’aide sur l’homonymie

Pour les articles homonymes, voir Moura (homonymie).

Cet article est une ébauche concernant l’informatique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

Leonardo de Moura
une illustration sous licence libre serait bienvenue
Biographie
Formation
Activités
Informaticien, mathématicienVoir et modifier les données sur Wikidata
Autres informations
A travaillé pour
Microsoft ResearchVoir 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
Prix Herbrand ()Voir et modifier les données sur Wikidata

modifier - modifier le code - modifier WikidataDocumentation du modèle

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

  • Ressources relatives à la rechercheVoir et modifier les données sur Wikidata :
    • Digital Bibliography & Library Project
    • Google Scholar
    • Mathematics Genealogy Project
    • ORCID
    • ResearchGate
    • Scopus
  • Notices d'autoritéVoir et modifier les données sur Wikidata :
    • VIAF
    • LCCN
    • Israël
    • WorldCat
  • icône décorative Portail des mathématiques
  • icône décorative Portail de la programmation informatique
  • icône décorative Portail de Microsoft