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 Z310: 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)



