Leonardo de Moura, Ph.D.

De Moura is a senior principal applied scientist in the Automated Reasoning Group at Amazon Web Services. In his spare time, he dedicates himself to serving as the chief architect and a board member of the Lean Focused Research Organization, a nonprofit organization he co-founded with Sebastian Ullrich. Before joining AWS in 2023, he was a senior principal researcher in the RiSE group at Microsoft Research and a computer scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, the boolean satisfiability problem and satisfiability modulo theories. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. His work in automated reasoning has been acknowledged with several prestigious awards, including the CAV Award, the Haifa Award, the Herbrand Award and the ACM’s Programming Languages Software Award.