Write a Blog >>
Nikolaj Bjørner

Registered user since Thu 15 Nov 2018

Name: Nikolaj Bjørner

Bio: 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.

Country: United States

Affiliation: Microsoft Research

Contributions

PADL 2020Invited Speaker of Invited Talk: Logical Engines for Cloud Configurations within the PADL 2020-track
Author of Panel: Programming with logic for the masses within the PADL 2020-track
VMCAI 2020Session Chair of Papers 5 (part of VMCAI 2020)
PC Member in Program Committee within the VMCAI 2020-track
Author of Solving LIA* Using Approximations within the VMCAI 2020-track
Show activities from other conferences

POPL 2020-profile
View general profile