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


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

POPL 2020-profile
View general profile