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 

• CADE 2009 (PC)
• CAV 2009 (PC)
• WING 2009 (PC)
• ICEGOV2008 - 2nd International Conference on Theory and Practice of Electronic Governance (PC)
• Dagstuhl Seminar on SMT solvers in Soft-, Hard- and Bio-ware, Spring 2010, (co-organizer)

Links

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

Recent Papers and Reports

• Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi. Modular difference logic is hard MSR-TR-2008-140
• Nikolaj Bjørner, Leonardo de Moura and Nikolai Tillmann Satisfiability Modulo Bit-precise Theories for Program Exploration Invited workshop paper, to appear at CFV 2008. Power point Slides
• Leonardo de Moura and Nikolaj Bjørner Engineering DPLL(T) + Saturation. IJCAR 2008
• Leonardo de Moura, Ruzica Piskac and Nikolaj Bjørner Deciding Effectively Propositional Logic using DPLL and Substitution Sets. Conference version at IJCAR 2008 Power Point slides.
• Dries Vanoverberghe, Nikolaj Bjørner, Jonathan de Halleux, Wolfram Schulte, Nikolai Tillmann Using Dynamic Symbolic Execution to Improve Deductive Verification Invited paper, SPIN 2008.
• Margus Veanes; Ando Saabas; Nikolaj Bjørner Bounded Reachability of Model Programs
• Margus Veanes, Nikolaj Bjørner, Alexander Raschke An SMT Approach to Bounded Reachability Analysis of Model Programs. FORTE 2008: 53-68
• Leonardo de Moura and Nikolaj Bjørner Z3: An Efficient SMT Solver 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.

Slides

• MSR India Summer School, Bangalore June 24-28, 2008 lecture 1 lecture 2 lecture 3 lecture 4 lecture 5 Lab exercises

Old workshops and conferences

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