Portrait of Nikolaj Bjorner

Nikolaj Bjorner

Principal Researcher

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 and test case generation.  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 and George Varghese introduced me the networking. 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, Sharing Folders and Meetings Space.  I also designed some of the chunking utilities used in the remote differential compression protocol RDC.

Recent Papers and Reports

Recent Papers and Reports

  • Scaling Network Verification 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 Conflicts 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.
  • 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, 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 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 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. 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 2011In 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
  • 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.
  • 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, 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

Conferences and Workshops

Links

Links

Slides

Slides

Old Workshops and Conferences

Old Workshops and Conferences

Follow us:

Share this page: