Nikolaj’s main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS, and the ETAPS test of time award. Leonardo 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. A prolific application is around Network Verification as deployed in the SecGuru tool in Microsoft Azure. In previous work in the Windows File Systems group, he developed the Distributed File System Replication, DFS-R, protocol. He studied at DTU, DIKU; and for his Master’s and PhD at Stanford.