Nikolaj Bjorner
Principal Researcher
About
I have the fortune to work with many inspiring colleagues. With Leonardo de Moura and Christoph Wintersteiger. I work on a state-of-the-art SMT constraint solver Z3. Z3 is used for program verification and test case generation. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS. 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.
