Research
My areas of interesting include automated reasoning, theorem proving, decision procedures, satisfiability (SAT) and satisfiability modulo theories (SMT). My main project is the Lean theorem prover. The Lean project aims to bring the automated and interactive theorem proving worlds together. One of the main goals is to provide a powerful system for reasoning about complex systems and mathematics, and verifying claims about both.
I also worked on Z3. Z3 is a very efficient SMT solver, it has builtin support for many useful theories such as: linear real and integer arithmetic, nonlinear real arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools.
Leonardo de Moura
Senior Principal Applied Scientist in the Automated Reasoning Group at AWS
leodemoura0@gmail.com
