BIO:
Nikolaj Bjorner is a senior researcher in the Research in Software Engineering group at Microsoft Research, Redmond. His main line of work is around the state-of-the-art SMT constraint solver Z3 with Leonardo de Moura. Z3 is used for program verification and test case generation. In his previous lives he wrote STeP, the Stanford Temporal Prover, and he was in the Core File Systems group where he designed and implemented the core of the distributed file replication system, DFS-R, and the content dependent chunking algorithms in the remote differential compression protocol RDC.