Portrait of Nikolaj Bjorner

Nikolaj Bjorner

Principal Researcher

Other

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