About Me

I’m a Senior 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 an open source theorem prover and programming language. Sebastian Ullrich and I are currently developing the next version (Lean 4). 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.


You can find more about me at: