I work with Leonardo de Moura on a state-of-the-art 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 the remote differential compression protocol RDC.

 Try out Z3 online

Recent Papers and Reports

• On Solving Universally Quantified Horn Clauses. Nikolaj Bjørner, Ken Mcmillan and Andrey Rybalchenko. SAS 2013
• Journal of Automated Deduction, Preface to a special issue dedicated to CADE 23. Nikolaj Bjørner, Viorica Sofronie-Stokkermans.
• Program Verification as Satisfiability Modulo Theories. Nikolaj Bjørner, Ken McMillan, Andrey Rybalchenko. SMT workshop 2012. Slides
• An SMT-LIB Format for Sequences and Regular Expressions. Nikolaj Bjørner, Vijay Ganesh, Raphael Michel, Margus Veanes. SMT workshop 2012.
• Anatomy of Alternating Quantifier Satisfiability. Anh-Dung Phan, Nikolaj Bjørner, David Monniaux. SMT workshop 2012.
• Taking Satisfiability to the Next Level with Z3. Nikolaj Bjørner. Invited talk, IJCAR 2012.
• Generalized Property Directed Reachability. Krystof Hoder and Nikolaj Bjørner. In SAT 2012.
• Tractability and Modern Satisfiability Modulo Theories Solvers. Nikolaj Bjørner and Leonardo de Moura. To appear in Handbook of Tractability. Editors: Lucas Bordeaux, Youssef Hamadi, Pushmeet Kohli, Robert Mateescu. Cambridge University Press.
• Latent Fault Detection in Cloud Services, Mickey Gabel, Assaf Schuster, Ran Gilad-Bachrach, Nikolaj Bjørner. In DSN 2012.
• Symbolic Automata: The Toolkit, Margus Veanes and Nikolaj Bjørner, in TACAS'12, Springer Verlag, March 2012
• Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Nikolaj Bjørner, Andrei Voronkov. Proceedings Springer 2012
• From Primal Infon Logic with Individual Variables to Datalog Nikolaj Bjørner, Guido de Caso and Yuri Gurevich Microsoft Research Technical Report MSR-TR-2011-84, July 2011
  To appear in Vladimir Lifschitz Festschrift
• Symbolic Finite State Transducers: Algorithms and Applications. Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjørner, in POPL’12, ACM SIGPLAN, January 2012
• Foreword to special issue dedicated to WING, Workshop on invariant generation, Journal of Symbolic Computation 2012. Editors Nikolaj Bjørner and Laura Kovacs.
• Engineering Theories with Z3. Nikolaj Bjørner. Invited talk, APLAS 2011.
• Foundations of Symbolic Tree Transducers. Margus Veanes and Nikolaj Bjørner. Bulletin of the EATCS, October 2011.
• Satisfiability Modulo Theories: Introduction and Applications. Leonardo de Moura, Nikolaj Bjørner. Communications of the ACM, September 2011.
• Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Nikolaj Bjørner, Viorica Sofronie-Stokkermans. Proceedings. Springer 2011
• µZ - An Efficient Engine for Fixed-Points with Constraints. Krystof Hoder, Nikolaj Bjørner and Leonardo de Moura. CAV 2011.
• Applications and Challenges in Satisfiability Modulo Theories. Leonardo de Moura and Nikolaj Bjørner. To appear in the First EasyChair Volume on WING (Workshop on Invariant Generation).
• Canonical Regular Types. Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte. ICLP-2011.
• Symbolic Tree Transducers. Margus Veanes, Nikolaj Bjørner. PSI-2011.
• Symbolic Transducers. Margus Veanes, Nikolaj Bjørner. MSR-TR
• Alternating Simulation and IOCO, Margus Veanes, Nikolaj Bjørner. ICTSS 2010
• Symbolic Automata Constraint Solving. Margus Veanes, Nikolaj Bjørner, Leonardo de Moura. LPAR (Yogyakarta) 2010.
• DKAL and Z3: A Logic Embedding Experiment. Sergio Mera, Nikolaj Bjørner. Fields of Logic and Computation 2010: 504-528.
• Linear Quantifier Elimination as an Abstract Decision Procedure. Nikolaj Bjørner. IJCAR 2010.
• Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. Leonardo de Moura, Nikolaj Bjørner. IJCAR 2010.
• TAPAS Theory Combinations and Practical Applications. Nikolaj Bjørner and Leonardo de Moura. Invited talk at FORMATS 2009. (Slides)
• Generalized, Efficient Array Decision Procedures. Leonardo de Moura, Nikolaj Bjørner. FMCAD 2009. Extended version in MSR-TR-121.
• Specifying and Composing Non-functional Requirements in Model-Based Development. Ethan K. Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte. Software Composition 2009: 72-89.

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

• Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis (MSR-TR-2009-57). Yannick Moy, Nikolaj Bjørner, Dave Sielaff. A workshop paper on the bit-precise aspects "Sound, Efficient, Bit-precise Static Analysis" appeared at CFV 2009.

• Input-Output Model Programs (MSR-TR-2009-56) Margus Veanes, Nikolaj Bjørner. ICTAC 2009.

• Symbolic Bounded Conformance Checking of Model Programs (MSR-TR-2009-28) Appeared at PSI 2009. Margus Veanes, Nikolaj Bjørner
• Symbolic Bounded Model Checking of Abstract State Machines (MSR-TR-2009-14) Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte.
• Linear Functional Fixed-points (MSR-TR-2009-8). Nikolaj Bjørner and Joe Hendrix. Revised conference version at CAV 2009. Slides
• RAP - Resource Adaptive Programming with an application to robust and fast file copying. Utkarsh Upadhyay and Nikolaj Bjørner.  PDF
• Deciding Effectively Propositional Logic with Equality Ruzica Piskac, Leonardo de Moura, Nikolaj Bjørner. 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.
• Proofs and Refutations, and Z3. Leonardo de Moura and Nikolaj Bjørner. IWIL 2008. PDF.
• Path Feasibility Analysis for String-Manipulating Programs Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov. MSR-TR-2008-153 (appeared at TACAS 2009).
• Modular difference logic is hard Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi. MSR-TR-2008-140
• Satisfiability Modulo Bit-precise Theories for Program Exploration Nikolaj Bjørner, Leonardo de Moura and Nikolai Tillmann. Invited workshop paper, to appear at CFV 2008. Power point Slides
• Engineering DPLL(T) + Saturation. Leonardo de Moura and Nikolaj Bjørner IJCAR 2008
• Deciding Effectively Propositional Logic using DPLL and Substitution Sets. Conference version at IJCAR 2008 Power Point slides. Leonardo de Moura, Ruzica Piskac and Nikolaj Bjørner
• Using Dynamic Symbolic Execution to Improve Deductive Verification Dries Vanoverberghe, Nikolaj Bjørner, Jonathan de Halleux, Wolfram Schulte, Nikolai Tillmann Invited paper, SPIN 2008.
• Bounded Reachability of Model Programs Margus Veanes; Ando Saabas; Nikolaj Bjørner
• An SMT Approach to Bounded Reachability Analysis of Model Programs. Margus Veanes, Nikolaj Bjørner, Alexander Raschke. FORTE 2008: 53-68
• Z3: An Efficient SMT Solver Leonardo de Moura and Nikolaj Bjørner TACAS, April 2008.
• Relevancy Propagation Leonardo de Moura and Nikolaj Bjørner. Technical Note, October 2007.
• Content-Dependent Chunking for Differential Compression, The Local Maximum Approach Nikolaj Bjørner, Andreas Blass, Yuri Gurevich. MSR-TR August 2007.
  Appears in Journal of Computer and System Sciences, Elsevier, 2009.
• Models and Software Model Checking for a Distributed File Replication System. Nikolaj Bjørner. Appears in Formal Methods and Hybrid Real-Time Systems September 2007: 1-23.
• Efficient E-matching for SMT solvers. Leonardo de Moura and Nikolaj Bjørner.  CADE 2007. PDF.
• Model-based Theory Combination. Leonardo de Moura and Nikolaj Bjørner. SMT 2007. PDF.
• Optimizing File Replication over Limited-Bandwidth Networks using Remote Differential Compression. Dan Teodosiu; Nikolaj Bjørner; Yuri Gurevich; Mark Manasse; Joe Porkka 2006.

Conferences and workshops 

• FLAIRS 26, Invited talk
• QBF workshop 2013 (PC)
• CAV 2013 (SAT/SMT Track chair)
• SYNASC 2013 (PC chair)
• ICFEM 2013 (PC)
• Dagstuhl Seminar: Deduction and Arithmetic (co-organizer with Rainer Hähnle, Tobias Nipkow, Christoph Weidenbach)
• FMCAD 2013 (PC)
• SCSS 2013 (PC)
• ICDCIT 2014 (PC)
• TACAS 2014 (Tool chair)

Links

• My very old home page.
• Foundations of Software Engineering Group's home page.
• RiSE: Research In Software Engineering.
• Horn Clause benchmarks
• Automata Benchmarks
• RiSE & SMT slides
• SecGuru benchmarks

Slides

• Formal Methods and Networks, Summer School, Ithaca June 10-14 2013
  • Lecture 1
  • Lecture 2
  • Lecture 3
  • Examples
• Verified Software Summer School, Shanghai, Aug 23-31, 2012
  Lecture 1 (August 29)
  Lecture 2 (August 30)
  Lecture 3 (August 31)
  Lecture 4 (August 31)
• 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

• FIMCP

• HCSS 2013, Keynote

• VMCAI 2013 (PC)

• ICFEM 2012 (PC)

• SYNASC 2012 (PC)

• YaC (Talk)

• Yandex (tech Talk)

• SEW-35 (PC)

• Dagstuhl Seminar, November 11-16 2012: Games & Decisions: Rigorous Systems Engineering (co-organizer with Laura Kovacs, Krishnendu Chatterjee, Rupak Majumdar)

• CPP 2012

• ASE 2012 (PC)

• ICEGOV 2012 (PC)

• Scandinavian Logic Symposium (Invited speaker), Roskilde Aug 20-21.

• DANSAS, Odense Aug 24. (Invited talk on Static analysis and verification as Satisfiability Modulo Theories). Slides.
• Turing-100 (PC)
• SMT 2012 (PC)
• WING 2012 (PC)
• AREIS 2012 (PC)
• SC 2012 (PC)
• CSL 2012 (PC)

• LPAR-18 (PC co-chair with Andrei Voronkov)

• IWIL 2012 (Invited Speaker)

• TAP 2012 (PC)

• NFM 2012 (PC)
• VMCAI 2012 (PC)

• Logic in CS workshop, Steklov Feb 1-3

• SMT/Z3 Course at DTU Jan 2-11

• APLAS+CPP 2011 (Keynote)

• Z3 SIG meeting MSR Cambridge (Nov 2-4)
• ASE 2011 (PC)
• Kutaisi 2011 (Invited speaker)
• Dagstuhl Seminar on SMT solvers in hard, soft and bio-ware. July 2011. (co-organizer)
• SC 2011 (PC)
• Software Engineering Workshop,
  Ireland 2011 (PC)
• CADE 2011 (PC co-chair with Viorica)
• ICFEM 2011 (PC)
• ICEGOV 2011 (PC)
• MIT Summer school on SAT/SMT (June 2011) (co-organizer)
• 1st HIPERFIT workshop: FORMULA & F*
• NFM 2011 (PC)
• TAP 2011 (PC)
• WRiSE 2011 (PC)
• Seminar on deduction at Scale, Ringberg. March 2011. (co-organizer)
  Photos
• TACAS 2011 (PC)
• POPL 2011 Tutorial on Theorem Proving Tools for Program Analysis
• ICDCIT 2011 (PC)
• ICGOV 2010 (PC)
• LPAR 17 (PC)
• CSL 2010 (PC)
• WING 2010 (chair with Laura Kovacs)
• SMT 2010 (PC)
• CASC 2010 (panel)
• IJCAR 2010 (PC)
• MSR Cambridge Workshop on Tractability(PPTX, PDF), July 5,6 2010.
• PLDI Tutorial on SMT/Z3
• Dagstuhl Seminar on SMT solvers in Soft-, Hard- and Bio-ware, Spring 2010, (co-organizer)
• NFM 2010 (invited speaker) (pptx,pdf)
• LPAR 16 (PC)
• QSIC 2010 (PC)
• ICDCIT 2010 (PC)
• FMCAD 2009 (Tutorial) (Slides)
• 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)