I'm a Principal Researcher in the RiSE group at Microsoft Research. I joined Microsoft in 2006, before that I was a Computer Scientist at SRI International. I obtained my PhD at PUC-Rio in 2000. My research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. I'm the main architect of Lean, Z3, Yices 1.0 and SAL. Lean is a new open source theorem prover that Soonho Kong and I are currently developing from scratch. Z3 and Yices are SMT solvers, and SAL (the Symbolic Analysis Laboratory) is an open source tool suite that includes symbolic and bounded model checkers, and automatic test generators. Z3 has been open sourced (under the MIT license) in the beginning of 2015. I received the Haifa Verification Conference Award in 2010. In 2014, the TACAS conference (Tools and Algorithms for the Construction and Analysis of Systems) gave me an award for "The most influential tool paper in the first 20 years of TACAS" to the Z3 paper: Z3: An Efficient SMT Solver. 14th International Conference, TACAS 2008, vol. 4963 of Lecture Notes in Computer Science. In 2015, Z3 received the Programming Languages Software Award from ACM SIGPLAN.