-
- 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 (opens in new tab). Nikolaj Bjorner, Nina Narodytska. IJCAI 2015.
- Property-Directed Inference of Universal Invariants or Proving Their Absence. (opens in new tab) 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. (opens in new tab) 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 (opens in new tab).
- 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 (opens in new tab). 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 (opens in new tab). 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 (opens in new tab).
- 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 (opens in new tab). 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 (opens in new tab). 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 (opens in new tab)
- 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 (opens in new tab), 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. (opens in new tab) 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 (opens in new tab)
- µ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 (opens in new tab).
- DKAL and Z3: A Logic Embedding Experiment. Sergio Mera, Nikolaj Bjørner. Fields of Logic and Computation 2010 (opens in new tab): 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 (opens in new tab). (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 (opens in new tab), Dirk Seifert (opens in new tab), Markus Dahlweid (opens in new tab), Thomas Santen (opens in new tab), Nikolaj Bjørner, Wolfram Schulte (opens in new tab). Software Composition 2009 (opens in new tab): 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 (opens in new tab).
- Symbolic Bounded Conformance Checking of Model Programs (MSR-TR-2009-28) Appeared at PSI 2009 (opens in new tab). 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 (opens in new tab). 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 (opens in new tab). PDF.
- Proofs and Refutations, and Z3. Leonardo de Moura and Nikolaj Bjørner. IWIL 2008 (opens in new tab). PDF.
- Path Feasibility Analysis for String-Manipulating Programs Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov. MSR-TR-2008-153 (appeared at TACAS 2009 (opens in new tab)).
- 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 (opens in new tab). Power point Slides
- Engineering DPLL(T) + Saturation. (opens in new tab) Leonardo de Moura and Nikolaj Bjørner IJCAR 2008
- Deciding Effectively Propositional Logic using DPLL and Substitution Sets. Conference version at IJCAR 2008 (opens in new tab) Power Point slides. Leonardo de Moura, Ruzica Piskac and Nikolaj Bjørner
- Using Dynamic Symbolic Execution to Improve Deductive Verification (opens in new tab) 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. (opens in new tab) 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. (opens in new tab)
- Models and Software Model Checking for a Distributed File Replication System. Nikolaj Bjørner. Appears in Formal Methods and Hybrid Real-Time Systems September (opens in new tab) 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.
-
-
- My very old home page (opens in new tab)
- RiSE: Research In Software Engineering.
- Automata Benchmarks
- RiSE & SMT slides
- SecGuru benchmarks
-
- Tutorial on Network Verification with George Varghese at SIGCOMM 2015.Slides, Demo
- Marktoberdorf summer school MOD-10-8-15 MOD-12-8-2015 MOD-14-8-2015
- VTSA 2014 summer school (lecturer)
- Slides 1, 2, 3
- FLAIRS (opens in new tab) 26, Invited talk
- Formal Methods and Networks, Summer School, Ithaca June 10-14 2013 (opens in new tab)
- Verified Software Summer School (opens in new tab), Shanghai, Aug 23-31, 2012Lecture 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)
-
- TASE 2015 (opens in new tab) (PC)
- FMCAD 2015 (PC) (opens in new tab)
- Dagstuhl seminar on Deduction: Extracting Information from Deduction, Models and Proofs. (opens in new tab) (co-organizer) (opens in new tab)
- SYNASC 2015 (opens in new tab) (Track chair for Logic and Programming)
- FM 2015 (opens in new tab) (PC co-chair)
- TAP 2015 (opens in new tab) (PC)
- QUANTIFY @ CADE 2015 (PC)
- AMI (opens in new tab) @ CADE 2015 (PC)
- ICFEM 2015 (opens in new tab) (PC)
- ICDCIT 2015 (invited speaker) (opens in new tab)
- Dagstuhl seminar on Formal Foundations of Networking (co-organizer
- ICFEM 2014 (invited speaker) (opens in new tab)
- SDN and NFV Conference (invited speaker)
- CAV 2014 (PC) (opens in new tab)
- FMCAD 2014 (PC) (opens in new tab)
- CSTVA 2014 (Invited speaker)
- HCVS 2014 (co organizer) (opens in new tab)
- TASE 2014 (PC) (opens in new tab)
- ECAI 2014 (external reviewer) (opens in new tab)
- SAT/SMT Summer School (lecturer) (opens in new tab)
- Software for Quantified Reasoning (co organizer) (opens in new tab)
- SSFT14, Menlo Park (opens in new tab)
- IMDEA, Microsoft workshop
- TACAS 2014 (Tool chair)
- NFM 2014 (PC) (opens in new tab)
- ReRISE winter school (lecturer) (opens in new tab)
- Dagstuhl Seminar: Deduction and Arithmetic (opens in new tab) (co-organizer with Rainer Hähnle, Tobias Nipkow, Christoph Weidenbach)
- FMCAD 2013 (PC) (opens in new tab)
- CAS 2013 (keynote) (opens in new tab)
- PAS 2013 (invited speaker) (opens in new tab)
- SCSS 2013 (opens in new tab) (PC)
- ICDCIT 2014 (opens in new tab) (PC)
- QBF workshop 2013 (opens in new tab) (PC)
- CAV 2013 (opens in new tab) (SAT/SMT Track chair)
- SYNASC 2013 (opens in new tab) (PC chair)
- ICFEM 2013 (PC) (opens in new tab)
- HOPA (opens in new tab)
- FIMCP (opens in new tab)
- HCSS (opens in new tab) 2013, Keynote
- VMCAI 2013 (PC)
- ICFEM 2012 (opens in new tab) (PC)
- SYNASC 2012 (opens in new tab) (PC)
- YaC (Talk)
- Yandex (tech Talk)
- SEW-35 (opens in new tab) (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 (opens in new tab) (PC)
- Scandinavian Logic Symposium (opens in new tab) (Invited speaker), Roskilde Aug 20-21.
- DANSAS (opens in new tab), Odense Aug 24. (Invited talk on Static analysis and verification as Satisfiability Modulo Theories). Slides.
- Turing-100 (opens in new tab) (PC)
- SMT 2012 (opens in new tab) (PC)
- WING 2012 (opens in new tab) (PC)
- AREIS 2012 (opens in new tab) (PC)
- SC 2012 (PC)
- CSL 2012 (opens in new tab) (PC)
- LPAR-18 (opens in new tab) (PC co-chair with Andrei Voronkov)
- IWIL 2012 (opens in new tab) (Invited Speaker)
- TAP (opens in new tab) 2012 (PC)
- NFM 2012 (opens in new tab) (PC)
- VMCAI (opens in new tab) 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 (opens in new tab) 2011 (PC)
- Kutaisi 2011 (opens in new tab) (Invited speaker)
- Dagstuhl Seminar on SMT solvers in hard, soft and bio-ware (opens in new tab). July 2011. (co-organizer)
- SC 2011 (opens in new tab) (PC)
- Software Engineering Workshop (opens in new tab),Ireland 2011 (PC)
- CADE 2011 (opens in new tab) (PC co-chair with Viorica (opens in new tab))
- ICFEM 2011 (opens in new tab) (PC)
- ICEGOV (opens in new tab)2011 (PC)
- MIT Summer school on SAT/SMT (opens in new tab)(June 2011) (co-organizer)
- 1st HIPERFIT (opens in new tab) workshop: FORMULA & F*
- NFM 2011 (opens in new tab) (PC)
- TAP 2011 (opens in new tab) (PC)
- WRiSE 2011 (opens in new tab) (PC)
- Seminar on deduction at Scale, Ringberg. March 2011. (co-organizer)Photos (opens in new tab)
- TACAS 2011 (opens in new tab) (PC)
- POPL 2011 Tutorial on Theorem Proving Tools for Program Analysis
- ICDCIT 2011 (PC)
- ICGOV 2010 (opens in new tab) (PC)
- LPAR 17 (opens in new tab) (PC)
- CSL 2010 (opens in new tab) (PC)
- WING 2010 (chair with Laura Kovacs)
- SMT 2010 (opens in new tab) (PC)
- CASC 2010 (opens in new tab) (panel)
- IJCAR 2010 (PC) (opens in new tab)
- MSR Cambridge Workshop on Tractability(PPTX, PDF), July 5,6 2010.
- PLDI Tutorial on SMT/Z3 (opens in new tab)
- Dagstuhl Seminar on SMT solvers in Soft-, Hard- and Bio-ware (opens in new tab), Spring 2010, (co-organizer)
- NFM 2010 (opens in new tab) (invited speaker) (pptx, pdf)
- LPAR 16 (opens in new tab) (PC)
- QSIC 2010 (opens in new tab) (PC)
- ICDCIT 2010 (PC)
- FMCAD 2009 (opens in new tab) (Tutorial) (Slides)
- SYNASC 2009 (opens in new tab) (Tutorial) (Slides)
- FORMATS 2009 (opens in new tab) (Invited speaker)
- CADE 2009 (opens in new tab) (PC)
- CAV 2009 (opens in new tab)(PC)
- RV 2009 (opens in new tab)(PC)
- CFV 2009 (opens in new tab)(Invited speaker)
- WING 2009 (opens in new tab)(PC)
- ICEGOV2008 – 2nd International Conference on Theory and Practice of Electronic Governance (opens in new tab)(PC)
- SMT in Program Analysis and Verification at IJCAR 2008 (tutorial co-organizer)
- Practical Aspects of Automated Reasoning (PAAR-2008) (opens in new tab)(PC)
- ESARM 08 (opens in new tab) (PC)
- SMT 2008 (PC)
- IJCAR 2008 (PC)
- MSR India Summer School on Programming Languages, Analysis and Verification (lecturer)
- CSR 2007 (PC)
- WING 2007 (opens in new tab) (PC)
- ESARLT 2007 (opens in new tab) (PC)
- LPAR 2007 (PC)
Nikolaj Bjørner
Partner Researcher