I have the fortune to work with many inspiring colleagues. With Leonardo de Moura and Christoph Wintersteiger I work on a state-of-the-art SMT constraint solver Z3. Z3 is used for program verification, including Rustan Leino's legendary Boogie tool, and test case generation, including Pex and SAGE. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS. Karthick Jayaraman and I created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure. With George Varghese I develop new techniques for Network Verification. 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 Spaces. I also designed some of the chunking utilities used in the remote differential compression protocol RDC.
Recent Papers and Reports
Satisfiability Modulo Theories, Nikolaj Bjørner, lecture notes, Marktoberdorf 2015. The notes elaborate on model and proof search in CDCL based SAT and SMT solvers. To appear in NATO Science for Peace and Security Series - D: Information and Communication Security 2016, Esparza, Grumberg and Seidl.
Scaling Network Veriﬁcation using Symmetry and Surgery. Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese. Preliminary version of paper to appear at POPL 2016.
ddNF: An Efficient Data Structure for Header Spaces. Nikolaj Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese. MSR-TR 2015.
On Conﬂicts and Strategies in QBF. Nikolaj Bjørner, Mikoláš Janota and William Klieber. Short Presentation Paper @ LPAR 20, Fiji, November 2015.
Playing with Quantified Satisfaction. Nikolaj Bjørner, Mikoláš Janota. Short Presentation Paper @ LPAR 20. Fiji, November 2015.
Maximum Satisfiability using Cores and Correction Sets. Nikolaj Bjorner, Nina Narodytska. IJCAI 2015.
Property-Directed Inference of Universal Invariants or Proving Their Absence. Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham. CAV 2015.
Horn Clause Solving for Program Verification. Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, Andrey Rybalchenko. YuriFest 75, Berlin 2015.
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.
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 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.
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. 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
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. 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
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.
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.
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.
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, 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
- 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
- Tutorial on Network Verification with George Varghese at SIGCOMM 2015.
- VTSA 2014 summer school (lecturer)
- Slides 1, 2, 3
- 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 Deduction: Extracting Information from Deduction, Models and Proofs. (co-organizer)
- SYNASC 2015 (Track chair for Logic and Programming)FM 2015 (PC co-chair)
- TAP 2015 (PC)
- QUANTIFY @ CADE 2015 (PC)
- AMI @ CADE 2015 (PC)
- ICFEM 2015 (PC)
- ICDCIT 2015 (invited speaker)
- Dagstuhl seminar on Formal Foundations of Networking (co-organizer
- ICFEM 2014 (invited speaker)
- SDN and NFV Conference (invited speaker)
- CAV 2014 (PC)
- 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
- IMDEA, Microsoft workshop
- TACAS 2014 (Tool chair)
- NFM 2014 (PC)
- ReRISE winter school (lecturer)
- 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)
- CAV 2013 (SAT/SMT Track chair)
- SYNASC 2013 (PC chair)
- ICFEM 2013 (PC)
- 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)
- 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)