Leonardo de Moura home about me publications slides research

About Me

Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold a position on the Board of Directors at the Lean FRO, where he actively contributes to its growth and development. Before joining AWS in 2023, he was a Senior Principal Researcher in the RiSE group at Microsoft Research, where he worked for 17 years starting in 2006. Prior to that, he worked as a Computer Scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo’s work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the Programming Languages Software Award by the ACM. Leo’s work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, and Nature News.

Awards

(2010) Haifa Verification Conference Award.
(2014) “The most influential tool paper in the first 20 years of TACAS” for the paper: Z3: An Efficient SMT Solver. (TACAS conference)
(2015) Programming Languages Software Award for Z3.
(2017) Skolem Award for the paper “Efficient E-Matching for SMT Solvers” that has passed the test of time, by being a most influential paper in the field.
(2018) Test of time award for the paper: Z3: An Efficient SMT Solver. (ETAPS conference)
(2019) Herbrand award for numerous and important contributions to SMT solving, including its theory, implementation, and application to a wide range of academic and industrial needs.
(2021) CAV Award for pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT).
(2021) Distinguished paper award at PLDI for the paper “Perceus: Garbage Free Reference Counting with Reuse”.

You can find more about me at: