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
Nikolaj Bjørner
Partner Researcher
论文与出版物
-
-
-
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
-
-
-
Arithmetic Solving in Z3
Nikolaj Bjørner, Lev Nachmanson
Computer Aided Verification (CAV 2024) | July 2024
-
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
作者：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
作者：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, 第 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, 第 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
-
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
-
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
-
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
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
-
Arithmetic Solving in Z3
Nikolaj Bjørner, Lev Nachmanson
Computer Aided Verification (CAV 2024) | July 2024
-
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, 第 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
-
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
-
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
-
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
-
Arithmetic Solving in Z3
Nikolaj Bjørner, Lev Nachmanson
Computer Aided Verification (CAV 2024) | July 2024
-
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.
-
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, 第 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
作者：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
作者：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
-
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
-
-
-
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
-
-
-
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
作者：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
作者：Microsoft
-
Checking Beliefs in Dynamic Networks
Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
MSR-TR-2014-58 | April 2014
作者：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
-
-
-
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
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
-
Arithmetic Solving in Z3
Nikolaj Bjørner, Lev Nachmanson
Computer Aided Verification (CAV 2024) | July 2024
-
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
-
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
-
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
-
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
-
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.
-
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
-
Checking Beliefs in Dynamic Networks
Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
MSR-TR-2014-58 | April 2014
作者：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
-
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
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
-