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 ACM SIGPLAN Programming Languages Software Award twice for Z3 and Lean.
Awards
-
(2014) "The most influential tool paper in the first 20 years of TACAS" for the paper: Z3: An Efficient SMT Solver. (TACAS conference)
-
(2015) ACM SIGPLAN 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.
-
(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.
-
(2021) CAV Award for pioneering contributions to the foundations of the theory and practice of SMT.
-
(2021) Distinguished paper award at PLDI for "Perceus: Garbage Free Reference Counting with Reuse".
-
(2025) Skolem Award for the paper "The Lean Theorem Prover" that has passed the test of time.
-
(2025) ACM SIGPLAN Programming Languages Software Award for Lean.