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
Nikolaj Bjørner
Partner Researcher
Publications
Publications by Year
-
-
Decentralized cloud wide-area network traffic engineering with BlastShield
Umesh Krishnaswamy, Rachee Singh, Nikolaj Bjørner, Himanshu Raj
MSR-TR-2021-31 | November 2021
Published by Microsoft
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
-
Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
Caleb Stanford, Margus Veanes, Nikolaj Bjørner
MSR-TR-2020-25 | August 2020
Published by Microsoft
Updated November 2020. Extended version of paper in PLDI'2021.
-
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
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
-
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, Vol 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
Cardinalities and Universal Quantifers for Verifying Parameterized Systems
Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
PLDI | June 2016
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
POPL | June 2016
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, Vol 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
Published by Microsoft
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
Published by Microsoft
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, Vol 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
Using Dynamic Symbolic Execution to Improve Deductive Verification
Nikolaj Bjørner, Wolfram Schulte, Nikolai Tillmann, 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
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
Publications by Research Area
-
Canonical Regular Types
Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
ICLP | January 2001
Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
Caleb Stanford, Margus Veanes, Nikolaj Bjørner
MSR-TR-2020-25 | August 2020
Published by Microsoft
Updated November 2020. Extended version of paper in PLDI'2021.
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
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, Vol 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
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
POPL | June 2016
Cardinalities and Universal Quantifers for Verifying Parameterized Systems
Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
PLDI | June 2016
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
Published by Microsoft
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
Published by Microsoft
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
Symbolic Tree Transducers
Margus Veanes, Nikolaj Bjørner
Ershov Informatics Conference (PSI'11) | January 2011
Canonical Regular Types
Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
ICLP (Technical Communications) | 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
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
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
-
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
Decentralized cloud wide-area network traffic engineering with BlastShield
Umesh Krishnaswamy, Rachee Singh, Nikolaj Bjørner, Himanshu Raj
MSR-TR-2021-31 | November 2021
Published by Microsoft
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
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
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
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
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
POPL | June 2016
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
Published by Microsoft
Checking Beliefs in Dynamic Networks
Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
MSR-TR-2014-58 | April 2014
Published by Microsoft
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
-
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
Symbolic Tree Automata
Margus Veanes, Nikolaj Bjørner
Information Processing Letters | March 2015, Vol 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
Published by Microsoft
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, Vol 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.
-
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
-
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
-
Using Dynamic Symbolic Execution to Improve Deductive Verification
Nikolaj Bjørner, Wolfram Schulte, Nikolai Tillmann, 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
MSR-TR-2007-75 | June 2007
Publications by Type
-
Canonical Regular Types
Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
ICLP | January 2001
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
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
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
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
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
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
POPL | June 2016
Cardinalities and Universal Quantifers for Verifying Parameterized Systems
Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
PLDI | June 2016
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
Symbolic Tree Transducers
Margus Veanes, Nikolaj Bjørner
Ershov Informatics Conference (PSI'11) | January 2011
Canonical Regular Types
Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte
ICLP (Technical Communications) | January 2011
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
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
Using Dynamic Symbolic Execution to Improve Deductive Verification
Nikolaj Bjørner, Wolfram Schulte, Nikolai Tillmann, Peli de Halleux
Proc. 15th International SPIN Workshop | January 2008
ISBN: 978-3-540-85113-4
-
Decentralized cloud wide-area network traffic engineering with BlastShield
Umesh Krishnaswamy, Rachee Singh, Nikolaj Bjørner, Himanshu Raj
MSR-TR-2021-31 | November 2021
Published by Microsoft
Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
Caleb Stanford, Margus Veanes, Nikolaj Bjørner
MSR-TR-2020-25 | August 2020
Published by Microsoft
Updated November 2020. Extended version of paper in PLDI'2021.
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
Published by Microsoft
Checking Beliefs in Dynamic Networks
Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
MSR-TR-2014-58 | April 2014
Published by Microsoft
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
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
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
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, Vol 64
Symbolic Tree Automata
Margus Veanes, Nikolaj Bjørner
Information Processing Letters | March 2015, Vol 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, Vol 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