I work with Leonardo de Moura and Christoph Wintersteiger on a state-of-the-art SMT constraint solver Z3. Z3 is used for program verification and test case generation. I also work with Karthick Jayaraman from Azure on validating firewalls using Z3. 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
- Horn Clause Solving for Program Verification. Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, Andrey Rybalchenko. Draft.
- Symbolic Tree Automata, Margus Veanes and Nikolaj Bjørner, Information Processing Letters, vol. 115, no. 3, pp. 418-424, Elsevier, March 2015
- Checking Cloud Contracts in Microsoft Azure. Nikolaj Bjørner and Karthick Jayaraman. Invited paper for ICDCIT February, 2015.
- Automated Analysis and Debugging of Network Connectivity Policies. Karthick Jayaraman, Nikolaj Bjorner, Geoff Outhred, and Charlie Kaufman
- nu-Z: An Optimizing SMT Solver. Nikolaj Bjørner and Anh-Dung Phan and Lars Fleckenstein. TACAS April 2015.
- Property Directed Polyhedral Abstraction. Nikolaj Bjørner and Arie Gurfinkel. VMCAI 2015.
- newZ: Maximal Satisfaction with Z3. Nikolaj Bjørner and Anh-Dung Phan. Invited paper, to appear in SCSS 2014.
- Computing All Implied Equalities via SMT-based Partition Refinement. Josh Berdine and Nikolaj Bjørner, IJCAR 2014. Technical Report.
- Monadic Decomposition. Margus Veanes, Nikolaj Bjørner, Lev Nachmanson and Sergey Bereg. CAV 2014.
- Property Directed Shape Analysis. Shachar Itzhaky, Nikolaj Bjørner, Thomas Reps, Mooly Sagiv, and Aditya Thakur. CAV 2014.
- Checking beliefs in Dynamic Networks. Nuno Lopes, Nikolaj Bjorner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. Technical Report. Revised version to appear in NSDI 2015.
- VeriCon: Towards Verifying Controller Programs in Software-Defined Networks. Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira and Asaf Valadarsky. PLDI 2014
- Software Engineering and Automated Deduction. Willem Visser, Nikolaj Bjørner, Natarajan Shankar. Future of Software Engineering session @ ICSE 2014.
- Instantiations, Zippers and EPR Interpolation. Nikolaj Bjørner, Konstantin Korovin, Arie Gurfinkel and Ori Lahav. Short paper at LPAR 19.
- Resourceful Reachability as HORN-LA. Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph Wintersteiger. LPAR 19.
- Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. Nikolaj Bjørner, Ken McMillan and Andrey Rybalchenko. In informal proceedings of HOPA 2013 (workshop on Higher-Order Program Analysis).
- 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 Quantiﬁer Satisﬁability. 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.
Z310: 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.
- 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.
Awarded The most influential tool paper in the first 20 years of TACAS at TACAS 2014.
- 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
- FM 2015 (PC co-chair)
- TAP 2015 (PC)
- QUANTIFY @ CADE 2015 (PC)
- AMI @ CADE 2015 (PC)
- ICFEM 2015 (PC)
- TASE 2015 (PC)
- FMCAD 2015 (PC)
- Dagstuhl seminar on Deduction: Extracting Information from Deduction, Models and Proofs. (co-organizer)
- SYNASC 2015 (Track chair for Logic and Programming)
- LPAR-20, 2015 (PC)
- ICDCIT 2016 (PC co-chair)
- My very old home page.
- RiSE: Research In Software Engineering.
- Horn Clause benchmarks
- Automata Benchmarks
- RiSE & SMT slides
- SecGuru benchmarks
- VTSA 2014 summer school (lecturer)
- FLAIRS 26, Invited talk
- Formal Methods and Networks, Summer School, Ithaca June 10-14 2013
- 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
- Dagstuhl seminar on Formal Foundations of Networking (co-organizer
- ICFEM 2014 (invited speaker)
- FMCAD 2014 (PC)
- CSTVA 2014 (Invited speaker)
- HCVS 2014 (co organizer)
- TASE 2014 (PC)
- ECAI 2014 (external reviewer)
- SAT/SMT Summer School (lecturer)
- Software for Quantified Reasoning (co organizer)
- SSFT14, Menlo Park
Dagstuhl Seminar: Deduction and Arithmetic (co-organizer with Rainer Hähnle, Tobias Nipkow, Christoph Weidenbach)
- FMCAD 2013 (PC)
- CAS 2013 (keynote)
- PAS 2013 (invited speaker)
- SCSS 2013 (PC)
- ICDCIT 2014 (PC)
- QBF workshop 2013 (PC)
- VMCAI 2013 (PC)
ICFEM 2012 (PC)
SYNASC 2012 (PC)
Yandex (tech Talk)
Dagstuhl Seminar, November 11-16 2012: Games & Decisions: Rigorous Systems Engineering (co-organizer with Laura Kovacs, Krishnendu Chatterjee, Rupak Majumdar)
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)
- 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)