Leonardo de Moura

Leonardo de Moura ist ein Informatiker und Entwickler des Z3 Theorem Prover[1] und des Lean Beweisassistent während seiner Zeit bei Microsoft Research.[2] Er arbeitet aktuell bei Amazon Web Services und ist der Chef-Softwarearchitekt bei Lean FRO.[3]

Er studierte Informatik an der Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), wo er 1996 den M.Sc. mit der Arbeit „Um sistema de programação visual“ erlangte. Er promovierte (D.Sc.) im Februar 2000 mit einer Dissertation über die formale Analyse und Verifikation von Programmen unter der Betreuung von Carlos José Pereira de Lucena.

Beruflicher Werdegang

Nach einer Tätigkeit als Computer Scientist am SRI International wechselte de Moura 2006 zu Microsoft Research in die RiSE-Gruppe, wo er u. a. den SMT-Solver Z3 und den Beweisassistenten Lean entwickelte. 2023 trat er der Automated Reasoning Group von Amazon Web Services bei und ist zugleich Chief Architect der Lean Focused Research Organization, einer Non-Profit-Organisation zur Weiterentwicklung von Lean.

Forschung und Softwareprojekte

De Moura ist Hauptentwickler mehrerer Werkzeuge des automatisierten Schließens und der formalen Verifikation:

  • Lean, ein interaktiver Beweisassistent und Programmiersprache, initialisiert 2013 bei Microsoft Research, mit Lean 4 seit 2021.
  • Z3, ein effizienter SMT-Solver für die Satisfiability Modulo Theories.
  • Beiträge zu Yices 1.0 und zum Symbolic Analysis Laboratory (SAL).

Seine Forschungsschwerpunkte liegen in der Entwicklung von Entscheidungsverfahren wie DPLL(T), Quantorenbehandlung (u. a. effizientes E-Matching) und der Kombination interaktiver und automatischer Beweisverfahren.

Auszeichnungen

  • 2010: Haifa Verification Conference Award[4]
  • 2014: TACAS „Most Influential Tool Paper (20 Jahre)“ für Z3: An Efficient SMT Solver
  • 2015: ACM SIGPLAN Programming Languages Software Award für Z3[5]
  • 2017: Skolem Award für Efficient E-Matching for SMT Solvers[6].
  • 2018: ETAPS Test of Time Award für Z3: An Efficient SMT Solver[7]
  • 2019: Herbrand Award (mit Nikolaj Bjørner) für Beiträge zum SMT-Lösen
  • 2021: CAV Award für Pionierleistungen im Bereich SMT[8]
  • 2025: ACM SIGPLAN Programming Languages Software Award für Lean[9]
  • 2025: Skolem Award für The Lean Theorem Prover (System Description)

Veröffentlichungen (Auswahl)

  • L. de Moura, N. Bjørner: Z3: An Efficient SMT Solver. In: TACAS 2008.
  • L. de Moura, S. Kong, J. Avigad, F. van Doorn, J. von Raumer: The Lean Theorem Prover (System Description). In: CADE-25, 2015.
  • L. de Moura, S. Ullrich: The Lean 4 theorem prover and programming language. In: CADE-28, 2021.

Einzelnachweise

  1. ↑ Alyssa Hughes: Model-based approach behind Z3 theorem prover’s efficiency, power. In: Microsoft Research. 16. Oktober 2019, abgerufen am 15. Juni 2025 (amerikanisches Englisch).
  2. ↑ Siobhan Roberts: A.I. Is Coming for Mathematics, Too In: The New York Times, 2. Juli 2023. Abgerufen am 15. Juni 2025 (amerikanisches Englisch). 
  3. ↑ Team — Lean FRO. In: lean-fro.org. Abgerufen am 16. Juni 2025 (englisch).
  4. ↑ Haifa Verification Conference 2010. Ehemals im Original (nicht mehr online verfügbar); abgerufen am 11. Februar 2020 (englisch).@1@2Vorlage:Toter Link/www.research.ibm.com (Seite nicht mehr abrufbar. Suche in Webarchiven)
  5. ↑ Programming Languages Software Award. Abgerufen am 11. Februar 2020 (englisch).
  6. ↑ Skolem Award. Abgerufen am 11. Februar 2020.
  7. ↑ Test of Time Award. 2018, abgerufen am 11. Februar 2020 (englisch).
  8. ↑ CAV Award | International Conference on Computer-Aided Verification. Archiviert vom Original am 1. Juni 2025; abgerufen am 1. Juni 2025 (englisch).
  9. ↑ Programming Languages Software Award. In: www.sigplan.org. Archiviert vom Original am 6. Juli 2025; abgerufen am 6. Juli 2025 (englisch).
Dieser Artikel wurde von Wikipedia herausgegeben. Der Text ist verfügbar unter Creative Commons Attribution-Share Alike 4.0, sofern nicht anders angegeben. Möglicherweise können weitere Bestimmungen für Mediendateien gelten.