Nikolaj Bjørner
Senior Principal Researcher
About
My main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 was developed with Leonardo de Moura, Lev Nachmanson and Christoph Wintersteiger. 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 I 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. Karthick Jayaraman and I created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure and George Varghese introduced me the networking. Until 2006, I was in the Core File Systems group where I designed and implemented the core of DFS-R which is included as part of Windows Server 2003 R2, Sharing Folders and Meetings Space. I also designed some of the chunking utilities used in the remote differential compression protocol RDC.