Nikolaj Bjørner

Nikolaj Bjørner is a Partner Researcher at Microsoft Research, affiliated with the Research in Software Engineering (RiSE) group. His work centers on symbolic solving techniques, particularly through the development of the Z3 SMT solver, which underpins program verification, test case generation, and cloud network management. He has also contributed to distributed file systems and network verification.

• Academic Rank: Researcher
• Key Collaborations: Leonardo de Moura (Z3), George Varghese (network verification), Mooly Sagiv (controller verification)

Research Interests: Bjørner’s work spans SMT solvers (Z3, muZ, SPACER), network verification (SecGuru, NoD, ddNF), and distributed systems (DFSR, RDC). His methods bridge logical reasoning, optimization, and network reliability.

Article Trends: His publications focus on SMT solving (e.g., Z3, muZ, SPACER), network verification (ddNF, TeaVar), and quantifier instantiation (MBQI). These works integrate model-based reasoning and theory combination to address scalability in software and networking.

Awards:

• 2021 ACM Fellow
• 2021 CAV Award (pioneering SMT contributions)
• 2019 Herbrand Award (Z3)
• 2017 Skolem Award (E-matching)
• 2016 Best Paper (HVC, ddNF)
• 2015 ACM SIGPLAN Software System Award (Z3)

Collaborations & Students: Bjørner has mentored interns and collaborators like Daniel Selsam (neural networks for SAT), Nuno P. Lopes (Alive, NoD), and Rachee Singh (Shoofly, traffic engineering). He co-organized the 2022 Shonan workshop on SAT and served as program chair for conferences like PSI and FMCAD.