Nikolaj Bjorner

Nikolaj Bjorner
PRINCIPAL RESEARCHER
.

I work with Leonardo de Moura and Christoph Wintersteiger on a state-of-the-art SMT constraint solver Z3.  Z3 is used for program verification and test case generation. I also work with Karthick Jayaraman from Azure on validating firewalls using Z3. 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

Conferences and workshops 

Links

Slides

Old workshops and conferences

        notes on SMT and Verification