Portrait of Nikolaj Bjorner

Nikolaj Bjorner

Principal Researcher


I have the fortune to work with many 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 and George Varghese introduced me to the networking. 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.


Network Verification

Established: February 1, 2014

Networks need to run reliably, efficiently, and without users noticing any problems, even as they grow. Keeping networks tuned this way requires the development of tools that improve the functioning of large-scale datacenter networks. This project investigates a range of network verification tools that help network operators and architects design, operate, maintain, troubleshoot, and report on their large networks. Specifically, the project explores three sub-areas: Data-plane verification Because networks forward packets according to their data…

Stubs – Lightweight Test Stubs for .NET

Established: March 19, 2009

Stubs is a lightweight framework for .NET that provides test stubs. For interfaces and non-sealed classes, type-safe wrappers are generated that can be easily customized by attaching delegates. Stubs are part of Moles, and work well together with Pex. Stubs is a lightweight framework for test stubs in .NET that is entirely based on delegates. Stubs may be used on interfaces, abstract classes or non-sealed classes. Stubs was designed provide a minimal overhead to the Pex white…

FORMULA – Modeling Foundations

Established: December 10, 2008

FORMULA 2.0: Formal Specifications for Verification and Synthesis Formula specifications are highly declarative logic programs that can express rich synthesis and verification problems. FORMULA 2.0 is framework for formally specifying domain-specific languages (DSLs) and model transformations. FORMULA specifications are succinct descriptions of DSLs, and specifications can be immediately connected to state-of-the-art analysis engines without additional expertise. FORMULA provides: (1) succinct specifications of DSLs and compilers, (2) efficient compilation…

Pex and Moles – Isolation and White box Unit Testing for .NET

Established: February 21, 2007

Pex automatically generates test suites with high code coverage using automated white box analysis. Pex is a Visual Studio add-in for testing .NET Framework applications. Moles supports unit testing by providing isolation by way of detours and stubs. The Moles framework is provided with Pex, or can be installed by itself as a Microsoft Visual Studio add-in. NEW: IntelliTest in Visual Studio 2015 is the evolution of Pex. IntelliTest is a feature integrated in Visual…














Link description



April 15, 2011


Nikolaj Bjorner, Joao Marques-Silva, and Youssef Hamadi


Microsoft Research, UCD, MSRC


Recent Papers and Reports

Recent Papers and Reports

Conferences and Workshops

Conferences and Workshops




Old Workshops and Conferences

Old Workshops and Conferences