Portrait of Nikolaj Bjorner

Nikolaj Bjorner

Principal Researcher

About

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.

Projects

Network Verification

Established: January 4, 2016

We are building a set of tools for dealing with network failures. Initial work with colleagues at Stanford includes an abstraction of the data plane of network boxes using a geometric model called Header Space. Using header space we have…

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…

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)…

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…

Publications

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

Projects

Other

Recent Papers and Reports

Recent Papers and Reports

Conferences and Workshops

Conferences and Workshops

Links

Slides

Slides

Old Workshops and Conferences

Old Workshops and Conferences