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. I am also managing the Foundations of Software Engineering group at Microsoft Research. 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.

Recent Papers and Reports

• Nikolaj Bjørner and Leonardo de Moura. TAPAS Theory Combinations and Practical Applications. Invited talk at FORMATS 2009. (Slides)
• Leonardo de Moura, Nikolaj Bjørner. Generalized, Efficient Array Decision Procedures. To appear at FMCAD 2009. Extended version in MSR-TR-121.

• Ethan K. Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte: Specifying and Composing Non-functional Requirements in Model-Based Development. Software Composition 2009: 72-89

• Nikolaj Bjørner and Leonardo de Moura Z3¹⁰: Applications, Enablers, Challenges and Directions. Invited paper for CFV 2009. (Slides)

• Yannick Moy, Nikolaj Bjørner, Dave Sielaff Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis (MSR-TR-2009-57). A workshop paper on the bit-precise aspects "Sound, Efficient, Bit-precise Static Analysis" appeared at CFV 2009.
• Margus Veanes, Nikolaj Bjørner Input-Output Model Programs (MSR-TR-2009-56) To appear at ICTAC 2009
• Margus Veanes, Nikolaj Bjørner Symbolic Bounded Conformance Checking of Model Programs (MSR-TR-2009-28) Appeared at PSI 2009.
• Margus VeanesNikolaj Bjørner, Yuri Gurevich, Wolfram Schulte. Symbolic Bounded Model Checking of Abstract State Machines (MSR-TR-2009-14)
• Nikolaj Bjørner and Joe Hendrix. Linear Functional Fixed-points (MSR-TR-2009-8). Revised conference version at CAV 2009. Slides
• Utkarsh Upadhyay and Nikolaj Bjørner. RAP - Resource Adaptive Programming with an application to robust and fast file copying. PDF
• Ruzica Piskac, Leonardo de Moura, Nikolaj Bjørner. Deciding Effectively Propositional Logic with Equality MSR-TR-2008-181.
• Nikolaj Bjørner, Bruno Dutertre and Leonardo de Moura. Accelerating Lemma Learning using Joins - DPPL(Join). Short paper at LPAR 2008. PDF.
• Leonardo de Moura and Nikolaj Bjørner. Proofs and Refutations, and Z3. IWIL 2008. PDF.
• Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov. Path Feasibility Analysis for String-Manipulating Programs MSR-TR-2008-153 (appeared at TACAS 2009).
• 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 MSR-TR August 2007.
  Appears in Journal of Computer and System Sciences, Elsevier, 2009.
• 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.

Conferences and workshops

• FMCAD 2009 (Tutorial)
• Dagstuhl Seminar on SMT solvers in Soft-, Hard- and Bio-ware, Spring 2010, (co-organizer)
• WING 2010 (chair with Laura Kovacs)
• ICDCIT 2010 (PC)
• IJCAR 2010 (PC)
• CSL 2010 (PC)
• QSIC 2010 (PC)
• SMT 2010 (PC)

Links

• My very old home page.
• Foundations of Software Engineering Group's home page.
• RiSE: Research In Software Engineering.

Slides

• MSR India Summer School, Bangalore June 24-28, 2008 lecture 1 lecture 2 lecture 3 lecture 4 lecture 5 Lab exercises
• UW Seminar, October 20, 2009. (Slides)

Old workshops and conferences

• SYNASC 2009 (Tutorial) (Slides)
• FORMATS 2009 (Invited speaker)
• CADE 2009 (PC)
• CAV 2009 (PC)
• RV 2009 (PC)
• CFV 2009 (Invited speaker)
• WING 2009 (PC)
• ICEGOV2008 - 2nd International Conference on Theory and Practice of Electronic Governance (PC)
• 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)