Prof. Nikolaj Bjorner

Title: Programming Constraint Services with Z3


Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Network Verification. His current main line of work with Leonardo de Moura and Christoph Wintersteiger is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award, most influential tool paper in the first 20 years of TACAS in 2014, the 2017 Skolem award for the 2007 paper on Efficient E-matching for SMT solvers. Another main line of activities are focused on Network Verification with colleagues in Azure, Karthick Jayaraman, and academia, George Varghese. Previously, he developed the DFSR, Distributed File System - Replication, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his Master's and Ph.D. degrees in computer science from Stanford University, and spent the first three years of university at DTU and DIKU.