Nikolaj Bjørner

Partner Researcher

出版物

表示方法:

- Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling
  
  Ruanqianqian (Lisa) Huang, Ayana Monroe, Jonathan "Peli" de Halleux, Sorin Lerner, Nikolaj Bjørner
  
  MSR-TR-2025-36 | June 2025
  
  Microsoft による投稿
  
  Publication
- PolySAT: Word-level Bit-vector Reasoning in Z3
  
  Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner, Laura Kov'acs
  
  International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2024) | May 2025
  
  Publication
- Arithmetic Solving in Z3
  
  Nikolaj Bjørner, Lev Nachmanson
  
  Computer Aided Verification (CAV 2024) | July 2024
  
  Publication
- CHISEL: An optical slice of the wide-area network
  
  Abhishek Vijaya Kumar, Bill Owens, Nikolaj Bjørner, Yawei Yin, Binbin Guan, Victor Bahl, Rachee Singh
  
  NSDI | April 2024
  
  Publication
- Decentralized cloud wide-area network traffic engineering with BlastShield
  
  Umesh Krishnaswamy, Rachee Singh, Nikolaj Bjørner, Himanshu Raj
  
  MSR-TR-2021-31 | November 2021
  
  Microsoft による投稿
  
  Publication
- Cost-effective capacity provisioning in wide area networks with Shoofly
  
  Rachee Singh, Nikolaj Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette
  
  ACM SIGCOMM 2021 | August 2021
  
  Publication
- Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
  
  Caleb Stanford, Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2020-25 | August 2020
  
  Microsoft による投稿
  
  Updated November 2020. Extended version of paper in PLDI'2021.
  
  Publication Author's Version プロジェクト
- TeaVaR: Striking the Right Utilization-Availability Balance in WAN Traffic Engineering
  
  Jeremy Bogle, Nikhil Bhatia, Manya Ghobadi, Ishai Menache, Nikolaj Bjørner, Asaf Valadarsky, Michael Schapira
  
  Sigcomm 2019 | August 2019
  
  Publication プロジェクト
- Validating datacenters at scale
  
  Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C. Bissonnette, Shane Foster, Andrew Helwer, M. Kasten, I. Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, N. Raje, Parag Sharma
  
  SIGCOMM 2019 | August 2019
  
  DOI Publication プロジェクト
- Optimizing Test Placement for Module-Level Regression Testing
  
  August Shi, Suresh Thummalapenta, Shuvendu Lahiri, Nikolaj Bjørner, Jacek Czerwonka
  
  Proceedings of the 39th International Conference on Software Engineering (ICSE'17) | May 2017
  
  公開日プロジェクト
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  Journal of the ACM | May 2017, 巻64
  
  公開日公開日公開日プロジェクト
- Automatically verifying reachability and well-formedness in P4 Networks
  
  Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, Andrey Rybalchenko
  
  MSR-TR-2016-65 | September 2016
  
  公開日
- ddNF: An Efficient Data Structure for Header Spaces
  
  Nikolaj Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese
  
  Haifa Verification Conference (HVC), 2016 | August 2016
  
  Publication プロジェクト
- Cardinalities and Universal Quantifers for Verifying Parameterized Systems
  
  Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
  
  PLDI | June 2016
  
  Publication
- Scaling Network Verification using Symmetry and Surgery
  
  Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
  
  POPL | June 2016
  
  Publication プロジェクト
- Scaling Network Veriï¬cation using Symmetry and Surgery
  
  Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
  
  Proc. of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) | January 2016
  
  公開日プロジェクト
- Symbolic Tree Automata
  
  Margus Veanes, Nikolaj Bjørner
  
  Information Processing Letters | March 2015, 巻115(3): pp. 418-424
  
  公開日公開日
- Automated Analysis and Debugging of Network Connectivity Policies
  
  Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, Charlie Kaufman
  
  MSR-TR-2014-102 | July 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  CAV'14 | July 2014
  
  公開日
- Checking Beliefs in Dynamic Networks
  
  Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
  
  MSR-TR-2014-58 | April 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Computing All Implied Equalities via SMT-based Partition Refinement
  
  Josh Berdine, Nikolaj Bjørner
  
  MSR-TR-2014-57 | April 2014
  
  公開日公開日公開日
- Resourceful Reachability as HORN-LA
  
  Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger
  
  International Conference on Logic for Programming, Artificial Intelligence and Reasoning | December 2013
  
  公開日
- Effectively Monadic Predicates
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  LPAR-19 | December 2013
  
  公開日
- Network Verification in the Light of Program Verification
  
  Nuno P. Lopes, Nikolaj Bjørner, Patrice Godefroid, George Varghese
  
  September 2013
  
  公開日
- On Solving Universally Quantified Horn Clauses
  
  Nikolaj Bjørner, Kenneth McMillan, Andrey Rybalchenko
  
  Static Analysis Symposium (SAS) | June 2013
  
  公開日公開日
- Open-World Logic Programs: A New Foundation for Formal Specifications
  
  Ethan Jackson, Wolfram Schulte, Nikolaj Bjørner
  
  MSR-TR-2013-55 | May 2013
  
  公開日
- Detecting Specification Errors in Declarative Languages with Constraints
  
  Ethan Jackson, Wolfram Schulte, Nikolaj Bjørner
  
  Model Driven Engineering Languages and Systems | September 2012
  
  公開日公開日
- Symbolic Automata: The Toolkit
  
  Margus Veanes, Nikolaj Bjørner
  
  TACAS'12 | March 2012
  
  公開日
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  公開日
- Alternating simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  International Journal on Software Tools for Technology Transfer (STTT) | September 2011
  
  公開日公開日
- From Primal Infon Logic with Individual Variables to Datalog
  
  Nikolaj Bjørner, Yuri Gurevich, Guido de Caso
  
  MSR-TR-2011-84 | July 2011
  
  公開日
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2011-85 | July 2011
  
  公開日
- Latent Fault Detection in Cloud Services
  
  Mickey Gabel, Ran Gilad-Bachrach, Nikolaj Bjørner, Assaf Schuster
  
  MSR-TR-2011-83 | July 2011
  
  公開日
- Symbolic Transducers
  
  Nikolaj Bjørner, Margus Veanes
  
  MSR-TR-2011-3 | January 2011
  
  公開日
- Canonical Regular Types
  
  Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
  
  ICLP (Technical Communications) | January 2011
  
  公開日プロジェクト
- Symbolic Tree Transducers
  
  Margus Veanes, Nikolaj Bjørner
  
  Ershov Informatics Conference (PSI'11) | January 2011
  
  公開日
- Content-Dependent Chunking for Differential Compression, The Local Maximum Approach
  
  Nikolaj Bjørner, Andreas Blass, Yuri Gurevich
  
  Journal of Computer and System Sciences | May 2010, 巻79(3-4): pp. 154-203
  
  公開日公開日
- Alternating Simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2010-38 | April 2010
  
  Extended version of paper with the same title in ICTSS 2010, LNCS vol 6435
  
  公開日
- Solving Extended Regular Constraints Symbolically
  
  Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
  
  MSR-TR-2009-177 | December 2009
  
  公開日プロジェクト
- Generalized, Efficient Array Decision Procedures
  
  Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2009-121 | September 2009
  
  A conference version of this report appears in the proceedings of FMCAD 2009.
  
  公開日
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  公開日プロジェクト
- Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis
  
  Yannick Moy, Nikolaj Bjørner, Dave Sielaff
  
  MSR-TR-2009-57 | May 2009
  
  公開日
- Input-Output Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-56 | May 2009
  
  Preliminary version of paper to appear in ICTAC'09, LNCS.
  
  公開日
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  公開日プロジェクト
- Linear Functional Fixed-points
  
  Nikolaj Bjørner, Joe Hendrix
  
  MSR-TR-2009-8 | January 2009
  
  公開日
- Path Feasibility Analysis for String-Manipulating Programs
  
  Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov
  
  Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009 | January 2009
  
  ISBN: 978-3-642-00767-5
  
  公開日公開日プロジェクトプロジェクト
- Specifying and Composing Non-functional Requirements in Model-Based Development
  
  Ethan Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte
  
  Proceedings of the 8th International Conference on Software Composition | January 2009
  
  公開日プロジェクト
- Deciding Effectively Propositional Logic with Equality
  
  Ruzica Piskac, Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2008-181 | December 2008
  
  公開日
- Modular difference logic is hard
  
  Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi
  
  MSR-TR-2008-140 | October 2008
  
  公開日
- Path Feasibility Analysis for String-Manipulating Programs
  
  Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov
  
  MSR-TR-2008-153 | October 2008
  
  公開日プロジェクトプロジェクト
- Deciding Effectively Propositional Logic using DPLL and Substitution Sets
  
  Leonardo de Moura, Ruzica Piskac, Nikolaj Bjørner
  
  MSR-TR-2008-104 | August 2008
  
  公開日公開日
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  公開日プロジェクトプロジェクト
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  公開日プロジェクト
- Z3: an efficient SMT solver
  
  Leonardo de Moura, Nikolaj Bjørner
  
  2008 Tools and Algorithms for Construction and Analysis of Systems | March 2008
  
  DOI PDF Publication Github プロジェクト
- Using Dynamic Symbolic Execution to Improve Deductive Verification
  
  Nikolaj Bjørner, Wolfram Schulte, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  Proc. 15th International SPIN Workshop | January 2008
  
  ISBN: 978-3-540-85113-4
  
  公開日公開日プロジェクトプロジェクト
- Relevancy Propagation
  
  Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2007-140 | October 2007
  
  公開日
- Models and Software Model Checking of a Distributed File Replication System
  
  Nikolaj Bjørner
  
  MSR-TR-2007-75 | June 2007
  
  公開日公開日
- Optimizing File Replication over Limited-Bandwidth Networks using Remote Differential Compression
  
  Dan Teodosiu, Nikolaj Bjørner, Yuri Gurevich, Mark Manasse, Joe Porkka
  
  MSR-TR-2006-157 | November 2006
  
  公開日公開日
- Canonical Regular Types
  
  Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
  
  ICLP | January 2001
  
  公開日

- PolySAT: Word-level Bit-vector Reasoning in Z3
  
  Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner, Laura Kov'acs
  
  International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2024) | May 2025
  
  Publication
- Arithmetic Solving in Z3
  
  Nikolaj Bjørner, Lev Nachmanson
  
  Computer Aided Verification (CAV 2024) | July 2024
  
  Publication
- TeaVaR: Striking the Right Utilization-Availability Balance in WAN Traffic Engineering
  
  Jeremy Bogle, Nikhil Bhatia, Manya Ghobadi, Ishai Menache, Nikolaj Bjørner, Asaf Valadarsky, Michael Schapira
  
  Sigcomm 2019 | August 2019
  
  Publication プロジェクト
- Symbolic Tree Automata
  
  Margus Veanes, Nikolaj Bjørner
  
  Information Processing Letters | March 2015, 巻115(3): pp. 418-424
  
  公開日公開日
- Automated Analysis and Debugging of Network Connectivity Policies
  
  Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, Charlie Kaufman
  
  MSR-TR-2014-102 | July 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  CAV'14 | July 2014
  
  公開日
- Effectively Monadic Predicates
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  LPAR-19 | December 2013
  
  公開日
- Network Verification in the Light of Program Verification
  
  Nuno P. Lopes, Nikolaj Bjørner, Patrice Godefroid, George Varghese
  
  September 2013
  
  公開日
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  公開日
- Alternating simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  International Journal on Software Tools for Technology Transfer (STTT) | September 2011
  
  公開日公開日
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2011-85 | July 2011
  
  公開日
- Symbolic Tree Transducers
  
  Margus Veanes, Nikolaj Bjørner
  
  Ershov Informatics Conference (PSI'11) | January 2011
  
  公開日
- Content-Dependent Chunking for Differential Compression, The Local Maximum Approach
  
  Nikolaj Bjørner, Andreas Blass, Yuri Gurevich
  
  Journal of Computer and System Sciences | May 2010, 巻79(3-4): pp. 154-203
  
  公開日公開日
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  公開日プロジェクト
- Input-Output Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-56 | May 2009
  
  Preliminary version of paper to appear in ICTAC'09, LNCS.
  
  公開日
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  公開日プロジェクト
- Arithmetic Solving in Z3
  
  Nikolaj Bjørner, Lev Nachmanson
  
  Computer Aided Verification (CAV 2024) | July 2024
  
  Publication
- Modular difference logic is hard
  
  Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi
  
  MSR-TR-2008-140 | October 2008
  
  公開日
- Deciding Effectively Propositional Logic using DPLL and Substitution Sets
  
  Leonardo de Moura, Ruzica Piskac, Nikolaj Bjørner
  
  MSR-TR-2008-104 | August 2008
  
  公開日公開日
- Canonical Regular Types
  
  Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
  
  ICLP | January 2001
  
  公開日
- Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling
  
  Ruanqianqian (Lisa) Huang, Ayana Monroe, Jonathan "Peli" de Halleux, Sorin Lerner, Nikolaj Bjørner
  
  MSR-TR-2025-36 | June 2025
  
  Microsoft による投稿
  
  Publication
- PolySAT: Word-level Bit-vector Reasoning in Z3
  
  Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner, Laura Kov'acs
  
  International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2024) | May 2025
  
  Publication
- Arithmetic Solving in Z3
  
  Nikolaj Bjørner, Lev Nachmanson
  
  Computer Aided Verification (CAV 2024) | July 2024
  
  Publication
- Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
  
  Caleb Stanford, Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2020-25 | August 2020
  
  Microsoft による投稿
  
  Updated November 2020. Extended version of paper in PLDI'2021.
  
  Publication Author's Version プロジェクト
- Validating datacenters at scale
  
  Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C. Bissonnette, Shane Foster, Andrew Helwer, M. Kasten, I. Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, N. Raje, Parag Sharma
  
  SIGCOMM 2019 | August 2019
  
  DOI Publication プロジェクト
- Optimizing Test Placement for Module-Level Regression Testing
  
  August Shi, Suresh Thummalapenta, Shuvendu Lahiri, Nikolaj Bjørner, Jacek Czerwonka
  
  Proceedings of the 39th International Conference on Software Engineering (ICSE'17) | May 2017
  
  公開日プロジェクト
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  Journal of the ACM | May 2017, 巻64
  
  公開日公開日公開日プロジェクト
- Automatically verifying reachability and well-formedness in P4 Networks
  
  Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, Andrey Rybalchenko
  
  MSR-TR-2016-65 | September 2016
  
  公開日
- ddNF: An Efficient Data Structure for Header Spaces
  
  Nikolaj Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese
  
  Haifa Verification Conference (HVC), 2016 | August 2016
  
  Publication プロジェクト
- Scaling Network Verification using Symmetry and Surgery
  
  Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
  
  POPL | June 2016
  
  Publication プロジェクト
- Cardinalities and Universal Quantifers for Verifying Parameterized Systems
  
  Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
  
  PLDI | June 2016
  
  Publication
- Scaling Network Veriï¬cation using Symmetry and Surgery
  
  Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
  
  Proc. of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) | January 2016
  
  公開日プロジェクト
- Automated Analysis and Debugging of Network Connectivity Policies
  
  Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, Charlie Kaufman
  
  MSR-TR-2014-102 | July 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  CAV'14 | July 2014
  
  公開日
- Checking Beliefs in Dynamic Networks
  
  Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
  
  MSR-TR-2014-58 | April 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Computing All Implied Equalities via SMT-based Partition Refinement
  
  Josh Berdine, Nikolaj Bjørner
  
  MSR-TR-2014-57 | April 2014
  
  公開日公開日公開日
- Resourceful Reachability as HORN-LA
  
  Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger
  
  International Conference on Logic for Programming, Artificial Intelligence and Reasoning | December 2013
  
  公開日
- On Solving Universally Quantified Horn Clauses
  
  Nikolaj Bjørner, Kenneth McMillan, Andrey Rybalchenko
  
  Static Analysis Symposium (SAS) | June 2013
  
  公開日公開日
- Open-World Logic Programs: A New Foundation for Formal Specifications
  
  Ethan Jackson, Wolfram Schulte, Nikolaj Bjørner
  
  MSR-TR-2013-55 | May 2013
  
  公開日
- Detecting Specification Errors in Declarative Languages with Constraints
  
  Ethan Jackson, Wolfram Schulte, Nikolaj Bjørner
  
  Model Driven Engineering Languages and Systems | September 2012
  
  公開日公開日
- Symbolic Automata: The Toolkit
  
  Margus Veanes, Nikolaj Bjørner
  
  TACAS'12 | March 2012
  
  公開日
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  公開日
- Alternating simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  International Journal on Software Tools for Technology Transfer (STTT) | September 2011
  
  公開日公開日
- From Primal Infon Logic with Individual Variables to Datalog
  
  Nikolaj Bjørner, Yuri Gurevich, Guido de Caso
  
  MSR-TR-2011-84 | July 2011
  
  公開日
- Symbolic Transducers
  
  Nikolaj Bjørner, Margus Veanes
  
  MSR-TR-2011-3 | January 2011
  
  公開日
- Canonical Regular Types
  
  Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
  
  ICLP (Technical Communications) | January 2011
  
  公開日プロジェクト
- Symbolic Tree Transducers
  
  Margus Veanes, Nikolaj Bjørner
  
  Ershov Informatics Conference (PSI'11) | January 2011
  
  公開日
- Alternating Simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2010-38 | April 2010
  
  Extended version of paper with the same title in ICTSS 2010, LNCS vol 6435
  
  公開日
- Solving Extended Regular Constraints Symbolically
  
  Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
  
  MSR-TR-2009-177 | December 2009
  
  公開日プロジェクト
- Generalized, Efficient Array Decision Procedures
  
  Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2009-121 | September 2009
  
  A conference version of this report appears in the proceedings of FMCAD 2009.
  
  公開日
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  公開日プロジェクト
- Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis
  
  Yannick Moy, Nikolaj Bjørner, Dave Sielaff
  
  MSR-TR-2009-57 | May 2009
  
  公開日
- Input-Output Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-56 | May 2009
  
  Preliminary version of paper to appear in ICTAC'09, LNCS.
  
  公開日
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  公開日プロジェクト
- Linear Functional Fixed-points
  
  Nikolaj Bjørner, Joe Hendrix
  
  MSR-TR-2009-8 | January 2009
  
  公開日
- Specifying and Composing Non-functional Requirements in Model-Based Development
  
  Ethan Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte
  
  Proceedings of the 8th International Conference on Software Composition | January 2009
  
  公開日プロジェクト
- Path Feasibility Analysis for String-Manipulating Programs
  
  Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov
  
  Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009 | January 2009
  
  ISBN: 978-3-642-00767-5
  
  公開日公開日プロジェクトプロジェクト
- Deciding Effectively Propositional Logic with Equality
  
  Ruzica Piskac, Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2008-181 | December 2008
  
  公開日
- Path Feasibility Analysis for String-Manipulating Programs
  
  Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov
  
  MSR-TR-2008-153 | October 2008
  
  公開日プロジェクトプロジェクト
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  公開日プロジェクトプロジェクト
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  公開日プロジェクト
- Z3: an efficient SMT solver
  
  Leonardo de Moura, Nikolaj Bjørner
  
  2008 Tools and Algorithms for Construction and Analysis of Systems | March 2008
  
  DOI PDF Publication Github プロジェクト
- Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling
  
  Ruanqianqian (Lisa) Huang, Ayana Monroe, Jonathan "Peli" de Halleux, Sorin Lerner, Nikolaj Bjørner
  
  MSR-TR-2025-36 | June 2025
  
  Microsoft による投稿
  
  Publication
- CHISEL: An optical slice of the wide-area network
  
  Abhishek Vijaya Kumar, Bill Owens, Nikolaj Bjørner, Yawei Yin, Binbin Guan, Victor Bahl, Rachee Singh
  
  NSDI | April 2024
  
  Publication
- Decentralized cloud wide-area network traffic engineering with BlastShield
  
  Umesh Krishnaswamy, Rachee Singh, Nikolaj Bjørner, Himanshu Raj
  
  MSR-TR-2021-31 | November 2021
  
  Microsoft による投稿
  
  Publication
- Cost-effective capacity provisioning in wide area networks with Shoofly
  
  Rachee Singh, Nikolaj Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette
  
  ACM SIGCOMM 2021 | August 2021
  
  Publication
- TeaVaR: Striking the Right Utilization-Availability Balance in WAN Traffic Engineering
  
  Jeremy Bogle, Nikhil Bhatia, Manya Ghobadi, Ishai Menache, Nikolaj Bjørner, Asaf Valadarsky, Michael Schapira
  
  Sigcomm 2019 | August 2019
  
  Publication プロジェクト
- Validating datacenters at scale
  
  Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C. Bissonnette, Shane Foster, Andrew Helwer, M. Kasten, I. Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, N. Raje, Parag Sharma
  
  SIGCOMM 2019 | August 2019
  
  DOI Publication プロジェクト
- Automatically verifying reachability and well-formedness in P4 Networks
  
  Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, Andrey Rybalchenko
  
  MSR-TR-2016-65 | September 2016
  
  公開日
- ddNF: An Efficient Data Structure for Header Spaces
  
  Nikolaj Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese
  
  Haifa Verification Conference (HVC), 2016 | August 2016
  
  Publication プロジェクト
- Scaling Network Verification using Symmetry and Surgery
  
  Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
  
  POPL | June 2016
  
  Publication プロジェクト
- Scaling Network Veriï¬cation using Symmetry and Surgery
  
  Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
  
  Proc. of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) | January 2016
  
  公開日プロジェクト
- Automated Analysis and Debugging of Network Connectivity Policies
  
  Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, Charlie Kaufman
  
  MSR-TR-2014-102 | July 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Checking Beliefs in Dynamic Networks
  
  Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
  
  MSR-TR-2014-58 | April 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Latent Fault Detection in Cloud Services
  
  Mickey Gabel, Ran Gilad-Bachrach, Nikolaj Bjørner, Assaf Schuster
  
  MSR-TR-2011-83 | July 2011
  
  公開日
- Optimizing File Replication over Limited-Bandwidth Networks using Remote Differential Compression
  
  Dan Teodosiu, Nikolaj Bjørner, Yuri Gurevich, Mark Manasse, Joe Porkka
  
  MSR-TR-2006-157 | November 2006
  
  公開日公開日
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  公開日
- Symbolic Transducers
  
  Nikolaj Bjørner, Margus Veanes
  
  MSR-TR-2011-3 | January 2011
  
  公開日
- Latent Fault Detection in Cloud Services
  
  Mickey Gabel, Ran Gilad-Bachrach, Nikolaj Bjørner, Assaf Schuster
  
  MSR-TR-2011-83 | July 2011
  
  公開日
- Using Dynamic Symbolic Execution to Improve Deductive Verification
  
  Nikolaj Bjørner, Wolfram Schulte, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  Proc. 15th International SPIN Workshop | January 2008
  
  ISBN: 978-3-540-85113-4
  
  公開日公開日プロジェクトプロジェクト
- Relevancy Propagation
  
  Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2007-140 | October 2007
  
  公開日
- Models and Software Model Checking of a Distributed File Replication System
  
  Nikolaj Bjørner
  
  MSR-TR-2007-75 | June 2007
  
  公開日公開日

- Canonical Regular Types
  
  Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
  
  ICLP | January 2001
  
  公開日
- PolySAT: Word-level Bit-vector Reasoning in Z3
  
  Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner, Laura Kov'acs
  
  International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2024) | May 2025
  
  Publication
- Arithmetic Solving in Z3
  
  Nikolaj Bjørner, Lev Nachmanson
  
  Computer Aided Verification (CAV 2024) | July 2024
  
  Publication
- CHISEL: An optical slice of the wide-area network
  
  Abhishek Vijaya Kumar, Bill Owens, Nikolaj Bjørner, Yawei Yin, Binbin Guan, Victor Bahl, Rachee Singh
  
  NSDI | April 2024
  
  Publication
- Cost-effective capacity provisioning in wide area networks with Shoofly
  
  Rachee Singh, Nikolaj Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette
  
  ACM SIGCOMM 2021 | August 2021
  
  Publication
- TeaVaR: Striking the Right Utilization-Availability Balance in WAN Traffic Engineering
  
  Jeremy Bogle, Nikhil Bhatia, Manya Ghobadi, Ishai Menache, Nikolaj Bjørner, Asaf Valadarsky, Michael Schapira
  
  Sigcomm 2019 | August 2019
  
  Publication プロジェクト
- Validating datacenters at scale
  
  Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C. Bissonnette, Shane Foster, Andrew Helwer, M. Kasten, I. Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, N. Raje, Parag Sharma
  
  SIGCOMM 2019 | August 2019
  
  DOI Publication プロジェクト
- Optimizing Test Placement for Module-Level Regression Testing
  
  August Shi, Suresh Thummalapenta, Shuvendu Lahiri, Nikolaj Bjørner, Jacek Czerwonka
  
  Proceedings of the 39th International Conference on Software Engineering (ICSE'17) | May 2017
  
  公開日プロジェクト
- ddNF: An Efficient Data Structure for Header Spaces
  
  Nikolaj Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese
  
  Haifa Verification Conference (HVC), 2016 | August 2016
  
  Publication プロジェクト
- Scaling Network Verification using Symmetry and Surgery
  
  Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
  
  POPL | June 2016
  
  Publication プロジェクト
- Cardinalities and Universal Quantifers for Verifying Parameterized Systems
  
  Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
  
  PLDI | June 2016
  
  Publication
- Scaling Network Veriï¬cation using Symmetry and Surgery
  
  Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
  
  Proc. of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) | January 2016
  
  公開日プロジェクト
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  CAV'14 | July 2014
  
  公開日
- Resourceful Reachability as HORN-LA
  
  Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger
  
  International Conference on Logic for Programming, Artificial Intelligence and Reasoning | December 2013
  
  公開日
- Effectively Monadic Predicates
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  LPAR-19 | December 2013
  
  公開日
- Network Verification in the Light of Program Verification
  
  Nuno P. Lopes, Nikolaj Bjørner, Patrice Godefroid, George Varghese
  
  September 2013
  
  公開日
- On Solving Universally Quantified Horn Clauses
  
  Nikolaj Bjørner, Kenneth McMillan, Andrey Rybalchenko
  
  Static Analysis Symposium (SAS) | June 2013
  
  公開日公開日
- Detecting Specification Errors in Declarative Languages with Constraints
  
  Ethan Jackson, Wolfram Schulte, Nikolaj Bjørner
  
  Model Driven Engineering Languages and Systems | September 2012
  
  公開日公開日
- Symbolic Automata: The Toolkit
  
  Margus Veanes, Nikolaj Bjørner
  
  TACAS'12 | March 2012
  
  公開日
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Margus Veanes, Pieter Hooimeijer, David Molnar, Nikolaj Bjorner, Ben Livshits
  
  POPL'12 | January 2012
  
  公開日
- Canonical Regular Types
  
  Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
  
  ICLP (Technical Communications) | January 2011
  
  公開日プロジェクト
- Symbolic Tree Transducers
  
  Margus Veanes, Nikolaj Bjørner
  
  Ershov Informatics Conference (PSI'11) | January 2011
  
  公開日
- Specifying and Composing Non-functional Requirements in Model-Based Development
  
  Ethan Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte
  
  Proceedings of the 8th International Conference on Software Composition | January 2009
  
  公開日プロジェクト
- Path Feasibility Analysis for String-Manipulating Programs
  
  Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov
  
  Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009 | January 2009
  
  ISBN: 978-3-642-00767-5
  
  公開日公開日プロジェクトプロジェクト
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  公開日プロジェクトプロジェクト
- Z3: an efficient SMT solver
  
  Leonardo de Moura, Nikolaj Bjørner
  
  2008 Tools and Algorithms for Construction and Analysis of Systems | March 2008
  
  DOI PDF Publication Github プロジェクト
- Using Dynamic Symbolic Execution to Improve Deductive Verification
  
  Nikolaj Bjørner, Wolfram Schulte, Nikolai Tillmann, Jonathan "Peli" de Halleux
  
  Proc. 15th International SPIN Workshop | January 2008
  
  ISBN: 978-3-540-85113-4
  
  公開日公開日プロジェクトプロジェクト
- Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling
  
  Ruanqianqian (Lisa) Huang, Ayana Monroe, Jonathan "Peli" de Halleux, Sorin Lerner, Nikolaj Bjørner
  
  MSR-TR-2025-36 | June 2025
  
  Microsoft による投稿
  
  Publication
- Decentralized cloud wide-area network traffic engineering with BlastShield
  
  Umesh Krishnaswamy, Rachee Singh, Nikolaj Bjørner, Himanshu Raj
  
  MSR-TR-2021-31 | November 2021
  
  Microsoft による投稿
  
  Publication
- Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
  
  Caleb Stanford, Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2020-25 | August 2020
  
  Microsoft による投稿
  
  Updated November 2020. Extended version of paper in PLDI'2021.
  
  Publication Author's Version プロジェクト
- Automatically verifying reachability and well-formedness in P4 Networks
  
  Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, Andrey Rybalchenko
  
  MSR-TR-2016-65 | September 2016
  
  公開日
- Automated Analysis and Debugging of Network Connectivity Policies
  
  Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, Charlie Kaufman
  
  MSR-TR-2014-102 | July 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Checking Beliefs in Dynamic Networks
  
  Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
  
  MSR-TR-2014-58 | April 2014
  
  Microsoft による投稿
  
  Publication プロジェクト
- Computing All Implied Equalities via SMT-based Partition Refinement
  
  Josh Berdine, Nikolaj Bjørner
  
  MSR-TR-2014-57 | April 2014
  
  公開日公開日公開日
- Open-World Logic Programs: A New Foundation for Formal Specifications
  
  Ethan Jackson, Wolfram Schulte, Nikolaj Bjørner
  
  MSR-TR-2013-55 | May 2013
  
  公開日
- Symbolic Finite State Transducers: Algorithms and Applications
  
  Nikolaj Bjørner, Ben Livshits, David Molnar, Margus Veanes
  
  MSR-TR-2011-85 | July 2011
  
  公開日
- From Primal Infon Logic with Individual Variables to Datalog
  
  Nikolaj Bjørner, Yuri Gurevich, Guido de Caso
  
  MSR-TR-2011-84 | July 2011
  
  公開日
- Latent Fault Detection in Cloud Services
  
  Mickey Gabel, Ran Gilad-Bachrach, Nikolaj Bjørner, Assaf Schuster
  
  MSR-TR-2011-83 | July 2011
  
  公開日
- Symbolic Transducers
  
  Nikolaj Bjørner, Margus Veanes
  
  MSR-TR-2011-3 | January 2011
  
  公開日
- Alternating Simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2010-38 | April 2010
  
  Extended version of paper with the same title in ICTSS 2010, LNCS vol 6435
  
  公開日
- Solving Extended Regular Constraints Symbolically
  
  Margus Veanes, Nikolaj Bjørner, Leonardo de Moura
  
  MSR-TR-2009-177 | December 2009
  
  公開日プロジェクト
- Generalized, Efficient Array Decision Procedures
  
  Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2009-121 | September 2009
  
  A conference version of this report appears in the proceedings of FMCAD 2009.
  
  公開日
- Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis
  
  Yannick Moy, Nikolaj Bjørner, Dave Sielaff
  
  MSR-TR-2009-57 | May 2009
  
  公開日
- Input-Output Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-56 | May 2009
  
  Preliminary version of paper to appear in ICTAC'09, LNCS.
  
  公開日
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  公開日プロジェクト
- Linear Functional Fixed-points
  
  Nikolaj Bjørner, Joe Hendrix
  
  MSR-TR-2009-8 | January 2009
  
  公開日
- Deciding Effectively Propositional Logic with Equality
  
  Ruzica Piskac, Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2008-181 | December 2008
  
  公開日
- Path Feasibility Analysis for String-Manipulating Programs
  
  Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov
  
  MSR-TR-2008-153 | October 2008
  
  公開日プロジェクトプロジェクト
- Modular difference logic is hard
  
  Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi
  
  MSR-TR-2008-140 | October 2008
  
  公開日
- Deciding Effectively Propositional Logic using DPLL and Substitution Sets
  
  Leonardo de Moura, Ruzica Piskac, Nikolaj Bjørner
  
  MSR-TR-2008-104 | August 2008
  
  公開日公開日
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  公開日プロジェクト
- Relevancy Propagation
  
  Leonardo de Moura, Nikolaj Bjørner
  
  MSR-TR-2007-140 | October 2007
  
  公開日
- Models and Software Model Checking of a Distributed File Replication System
  
  Nikolaj Bjørner
  
  MSR-TR-2007-75 | June 2007
  
  公開日公開日
- Optimizing File Replication over Limited-Bandwidth Networks using Remote Differential Compression
  
  Dan Teodosiu, Nikolaj Bjørner, Yuri Gurevich, Mark Manasse, Joe Porkka
  
  MSR-TR-2006-157 | November 2006
  
  公開日公開日
- Monadic Decomposition
  
  Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg
  
  Journal of the ACM | May 2017, 巻64
  
  公開日公開日公開日プロジェクト
- Symbolic Tree Automata
  
  Margus Veanes, Nikolaj Bjørner
  
  Information Processing Letters | March 2015, 巻115(3): pp. 418-424
  
  公開日公開日
- Alternating simulation and IOCO
  
  Margus Veanes, Nikolaj Bjørner
  
  International Journal on Software Tools for Technology Transfer (STTT) | September 2011
  
  公開日公開日
- Content-Dependent Chunking for Differential Compression, The Local Maximum Approach
  
  Nikolaj Bjørner, Andreas Blass, Yuri Gurevich
  
  Journal of Computer and System Sciences | May 2010, 巻79(3-4): pp. 154-203
  
  公開日公開日
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  公開日プロジェクト

Nikolaj Bjørner

出版物

Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling

PolySAT: Word-level Bit-vector Reasoning in Z3

Arithmetic Solving in Z3

CHISEL: An optical slice of the wide-area network

Decentralized cloud wide-area network traffic engineering with BlastShield

Cost-effective capacity provisioning in wide area networks with Shoofly

Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints

TeaVaR: Striking the Right Utilization-Availability Balance in WAN Traffic Engineering

Validating datacenters at scale

Optimizing Test Placement for Module-Level Regression Testing

Monadic Decomposition

Automatically verifying reachability and well-formedness in P4 Networks

ddNF: An Efficient Data Structure for Header Spaces

Cardinalities and Universal Quantifers for Verifying Parameterized Systems

Scaling Network Verification using Symmetry and Surgery

Scaling Network Veriï¬cation using Symmetry and Surgery

Symbolic Tree Automata

Automated Analysis and Debugging of Network Connectivity Policies

Monadic Decomposition

Checking Beliefs in Dynamic Networks

Computing All Implied Equalities via SMT-based Partition Refinement

Resourceful Reachability as HORN-LA

Effectively Monadic Predicates

Network Verification in the Light of Program Verification

On Solving Universally Quantified Horn Clauses

Open-World Logic Programs: A New Foundation for Formal Specifications

Detecting Specification Errors in Declarative Languages with Constraints

Symbolic Automata: The Toolkit

Symbolic Finite State Transducers: Algorithms and Applications

Alternating simulation and IOCO

From Primal Infon Logic with Individual Variables to Datalog

Symbolic Finite State Transducers: Algorithms and Applications

Latent Fault Detection in Cloud Services

Symbolic Transducers

Canonical Regular Types

Symbolic Tree Transducers

Content-Dependent Chunking for Differential Compression, The Local Maximum Approach

Alternating Simulation and IOCO

Solving Extended Regular Constraints Symbolically

Generalized, Efficient Array Decision Procedures

Symbolic Bounded Model Checking of Abstract State Machines

Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis

Input-Output Model Programs

Symbolic Bounded Conformance Checking of Model Programs

Linear Functional Fixed-points

Path Feasibility Analysis for String-Manipulating Programs

Specifying and Composing Non-functional Requirements in Model-Based Development

Deciding Effectively Propositional Logic with Equality

Modular difference logic is hard

Path Feasibility Analysis for String-Manipulating Programs

Deciding Effectively Propositional Logic using DPLL and Substitution Sets

An SMT Approach to Bounded Reachability Analysis of Model Programs

Bounded reachability of model programs

Z3: an efficient SMT solver

Using Dynamic Symbolic Execution to Improve Deductive Verification

Relevancy Propagation

Models and Software Model Checking of a Distributed File Replication System

Optimizing File Replication over Limited-Bandwidth Networks using Remote Differential Compression

Canonical Regular Types

PolySAT: Word-level Bit-vector Reasoning in Z3

Arithmetic Solving in Z3

TeaVaR: Striking the Right Utilization-Availability Balance in WAN Traffic Engineering

Symbolic Tree Automata

Automated Analysis and Debugging of Network Connectivity Policies

Monadic Decomposition

Effectively Monadic Predicates

Network Verification in the Light of Program Verification

Symbolic Finite State Transducers: Algorithms and Applications

Alternating simulation and IOCO

Symbolic Finite State Transducers: Algorithms and Applications

Symbolic Tree Transducers

Content-Dependent Chunking for Differential Compression, The Local Maximum Approach

Symbolic Bounded Model Checking of Abstract State Machines

Input-Output Model Programs

Symbolic Bounded Conformance Checking of Model Programs

Arithmetic Solving in Z3

Modular difference logic is hard

Deciding Effectively Propositional Logic using DPLL and Substitution Sets

Scaling Network Veriï¬cation using Symmetry and Surgery

Scaling Network Veriï¬cation using Symmetry and Surgery

Scaling Network Veriï¬cation using Symmetry and Surgery