I am a researcher in the Foundations of Software Engineering Group.

Background

I am working with Leonardo de Moura on a next generation SMT constraint solver Z3. Z3 is used for program verification and test case generation. 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 RDC.

Conferences and workshops 

• SMT in Program Analysis and Verification at IJCAR 2008 (tutorial co-organizer)
• MSR India Summer School on Programming Languages, Analysis and Verification (lecturer)
• Practical Aspects of Automated Reasoning (PAAR-2008) (PC)
• SMT 2008 (PC)
• IJCAR 2008 (PC)

Links

• My very old home page.
• Foundations of Software Engineering Group's home page.

Recent Papers and Reports

• Leonardo de Moura and Nikolaj Bjørner Z3: An Efficient SMT Solver To appear in TACAS, April 2008.
• Leonardo de Moura and Nikolaj Bjørner Relevancy Propagation Technical Note, October 2007.
• Nikolaj Bjørner, Andreas Blass, Yuri Gurevich. Content-Dependent Chunking for Differential Compression, The Local Maximum Approach August 2007.
• Nikolaj Bjørner. Models and Software Model Checking for a Distributed File Replication System. Appears in Formal Methods and Hybrid Real-Time Systems September 2007: 1-23.
• Leonardo de Moura and Nikolaj Bjørner. Efficient E-matching for SMT solvers. CADE 2007. PDF.
• Leonardo de Moura and Nikolaj Bjørner. Model-based Theory Combination. SMT 2007. PDF.
• Dan Teodosiu; Nikolaj Bjørner; Yuri Gurevich; Mark Manasse; Joe Porkka Optimizing File Replication over Limited-Bandwidth Networks using Remote Differential Compression. 2006.

Old workshops and conferences

• CSR 2007 (PC)
• WING 2007 (PC)
• ESARLT 2007 (PC)
• LPAR 2007 (PC)