Nikolaj Bjorner is a Senior Researcher at Microsoft Research. Nikolaj's line of work is around the state-of-the-art SMT constraint solver Z3.  Z3 is used for program verification, test case generation among several applications. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS. Leonardo de Moura and Nikolaj received the Herbrand Award at CADE 2019, in recognition of numerous and important contributions to SMT solving, including its theory, implementation, and application to a wide range of academic and industrial needs. With Karthick Jayaraman he created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure. He also designed and implemented the core of DFS-R and parts of RDC, shipped in Windows Server products.