Leonardo de Moura ist ein Informatiker und Entwickler des Z3 Theorem Prover und des Lean Beweisassistenten während seiner Zeit bei Microsoft Research. Er arbeitet bei Amazon Web Services und ist der Chef-Softwarearchitekt bei Lean FRO.
Er studierte Informatik an der Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio).
Beruflicher Werdegang Seit 2006 arbeitete de Moura 2006 bei Microsoft Research in der 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 maschinengestützten Beweisens 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 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 2017: Skolem Award für Efficient E-Matching for SMT Solvers. 2018: ETAPS Test of Time Award für Z3: An Efficient SMT Solver 2019: Herbrand Award (mit Nikolaj Bjørner) für Beiträge zum SMT-Lösen 2021: CAV Award für Pionierleistungen im Bereich SMT 2025: ACM SIGPLAN Programming Languages Software Award für Lean 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.
Weblinks Persönliche Website Lean Focused Research Organization Publikationsliste bei DBLP Google-Scholar-Profil
Einzelnachweise
Kategorie:Informatiker Kategorie:Geboren im 20. Jahrhundert Kategorie:Mann