Leonardo de Moura

Leonardo de Moura ist ein brasilianischer 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:

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

Veröffentlichungen (Auswahl)

Normdaten (Person): LCCN: nb2013021148 | VIAF: 307438739 | Wikipedia-Personensuche | Kein GND-Datensatz. Letzte Überprüfung: 14. August 2025.