Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Nikolaj Bjorner

Nikolaj Bjorner
PRINCIPAL RESEARCHER
.

I have the fortune to work with may 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. 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, Windows Live Messenger (Sharing Folders), and Vista Meetings Space. I also designed some of the chunking utilities used in the remote differential compression protocol RDC.

Contact:

 nbjorner@microsoft.com

Recent Papers and Reports

  • Property-Directed Inference of Universal Invariants or Proving Their Absence. Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham.  CAV 2015. Download: PDF

  • Horn Clause Solving for Program Verification. Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, Andrey Rybalchenko. Draft.

Conferences and workshops 

Links

Slides

Old workshops and conferences

        notes on SMT and Verification