Nikolaj S. Bjørner

Orcid: 0000-0002-1695-2810

Affiliations:
  • Microsoft Research, Redmond, WA, USA
  • Stanford University, CA, USA (PhD 1998)


According to our database1, Nikolaj S. Bjørner authored at least 135 papers between 1995 and 2024.

Collaborative distances:
  • Dijkstra number2 of three.
  • Erdős number3 of two.

Awards

ACM Fellow

ACM Fellow 2021, "For contributions to SMT solvers and network verification".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
PolySAT: Word-level Bit-vector Reasoning in Z3.
CoRR, 2024

CHISEL: An optical slice of the wide-area network.
Proceedings of the 21st USENIX Symposium on Networked Systems Design and Implementation, 2024

2023
An Ethereum-compatible blockchain that explicates and ensures design-level safety properties for smart contracts.
CoRR, 2023

Satisfiability Modulo Custom Theories in Z3.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2023

OneWAN is better than two: Unifying a split WAN architecture.
Proceedings of the 20th USENIX Symposium on Networked Systems Design and Implementation, 2023

Scalable Optimal Layout Synthesis for NISQ Quantum Processors.
Proceedings of the 60th ACM/IEEE Design Automation Conference, 2023

On Incremental Pre-processing for SMT.
Proceedings of the Automated Deduction - CADE 29, 2023

2022
Algebra-Based Reasoning for Loop Synthesis.
Formal Aspects Comput., 2022

Traffic engineering: from ISP to cloud wide area networks.
Proceedings of the SOSR '22: The ACM SIGCOMM Symposium on SDN Research, Virtual Event, October 19, 2022

User-Propagators for Custom Theories in SMT Solving.
Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

Analysis of Core-Guided MaxSat Using Cores and Correction Sets.
Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

Decentralized cloud wide-area network traffic engineering with BLASTSHIELD.
Proceedings of the 19th USENIX Symposium on Networked Systems Design and Implementation, 2022

2021
Preface of the special issue on the conference on formal methods in computer aided design 2018.
Formal Methods Syst. Des., 2021

Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431).
Dagstuhl Reports, 2021

Cost-effective capacity provisioning in wide area networks with Shoofly.
Proceedings of the ACM SIGCOMM 2021 Conference, Virtual Event, USA, August 23-27, 2021., 2021

Symbolic Boolean derivatives for efficiently solving extended regular expression constraints.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Supercharging Plant Configurations Using Z3.
Proceedings of the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, 2021

2020
Solving $\mathrm {LIA} ^\star $ Using Approximations.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Navigating the Universe of Z3 Theory Solvers.
Proceedings of the Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, 2020

Algebra-Based Loop Synthesis.
Proceedings of the Integrated Formal Methods - 16th International Conference, 2020

2019
Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062).
Dagstuhl Reports, 2019

NeuroCore: Guiding High-Performance SAT Solvers with Unsat-Core Predictions.
CoRR, 2019

The Science, Art, and Magic of Constrained Horn Clauses.
Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2019


TEAVAR: striking the right utilization-availability balance in WAN traffic engineering.
Proceedings of the ACM Special Interest Group on Data Communication, 2019

Guiding High-Performance SAT Solvers with Unsat-Core Predictions.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Reversible Pebbling Game for Quantum Memory Management.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2019

2018
Editorial.
Formal Aspects Comput., 2018

Preface for the special issue "FM15".
Acta Informatica, 2018

Programming Z3.
Proceedings of the Engineering Trustworthy Software Systems - 4th International School, 2018

Constrained Image Generation Using Binarized Neural Networks with Decision Procedures.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Core-Guided Minimal Correction Set and Core Enumeration.
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

Z3 and SMT in Industrial R&D.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017
Monadic Decomposition.
J. ACM, 2017

Property-Directed Inference of Universal Invariants or Proving Their Absence.
J. ACM, 2017

Report on Networking and Programming Languages 2017.
Comput. Commun. Rev., 2017

Correct by Construction Networks Using Stepwise Refinement.
Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, 2017

Abduction by Non-Experts.
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Optimizing test placement for module-level regression testing.
Proceedings of the 39th International Conference on Software Engineering, 2017

Abduction for Learning Smart City Rules.
Proceedings of the GCAI 2017, 2017

2016
SMT Solvers: Foundations and Applications.
Proceedings of the Dependable Software Systems Engineering, 2016

Scaling network verification using symmetry and surgery.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Cardinalities and universal quantifiers for verifying parameterized systems.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

ddNF: An Efficient Data Structure for Header Spaces.
Proceedings of the Hardware and Software: Verification and Testing, 2016

AVATAR Modulo Theories.
Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

2015
Symbolic tree automata.
Inf. Process. Lett., 2015

Formal Foundations for Networking (Dagstuhl Seminar 15071).
Dagstuhl Reports, 2015

Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381).
Dagstuhl Reports, 2015

Property Directed Polyhedral Abstraction.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

νZ - An Optimizing SMT Solver.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Checking Beliefs in Dynamic Networks.
Proceedings of the 12th USENIX Symposium on Networked Systems Design and Implementation, 2015

On Conflicts and Strategies in QBF.
Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

Playing with Quantified Satisfaction.
Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

Maximum Satisfiability Using Cores and Correction Sets.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Checking Cloud Contracts in Microsoft Azure.
Proceedings of the Distributed Computing and Internet Technology, 2015

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Equivalence of Finite-Valued Symbolic Finite Transducers.
Proceedings of the Perspectives of System Informatics, 2015

Horn Clause Solvers for Program Verification.
Proceedings of the Fields of Logic and Computation II, 2015

2014
νZ - Maximal Satisfaction with Z3.
Proceedings of the 6th International Symposium on Symbolic Computation in Software Science, 2014

VeriCon: towards verifying controller programs in software-defined networks.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Software engineering and automated deduction.
Proceedings of the on Future of Software Engineering, 2014

Property-Directed Shape Analysis.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Computing All Implied Equalities via SMT-Based Partition Refinement.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

Tractability and Modern Satisfiability Modulo Theories Solvers.
Proceedings of the Tractability: Practical Approaches to Hard Problems, 2014

2013
Preface: Special Issue of Selected Extended Papers of CADE-23.
J. Autom. Reason., 2013

Deduction and Arithmetic (Dagstuhl Seminar 13411).
Dagstuhl Reports, 2013

Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types.
CoRR, 2013

Satisfiability modulo theories for high integrity development.
Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, 2013

On Solving Universally Quantified Horn Clauses.
Proceedings of the Static Analysis - 20th International Symposium, 2013

Effectively Monadic Predicates.
Proceedings of the LPAR 2013, 2013

Instantiations, Zippers and EPR Interpolation.
Proceedings of the LPAR 2013, 2013

Resourceful Reachability as HORN-LA.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Invited Talk Abstracts.
Proceedings of the Twenty-Sixth International Florida Artificial Intelligence Research Society Conference, 2013

2012
Alternating simulation and IOCO.
Int. J. Softw. Tools Technol. Transf., 2012

Foreword.
J. Symb. Comput., 2012

Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461).
Dagstuhl Reports, 2012

Symbolic Automata: The Toolkit.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials.
Proceedings of the Model Checking Software - 19th International Workshop, 2012

Generalized Property Directed Reachability.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Symbolic finite state transducers: algorithms and applications.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Detecting Specification Errors in Declarative Languages with Constraints.
Proceedings of the Model Driven Engineering Languages and Systems, 2012

Engineering Theories with Z3.
Proceedings of the IWIL 2012: The 9th International Workshop on the Implementation of Logics, 2012

SMT in Verification, Modeling, and Testing at Microsoft.
Proceedings of the Hardware and Software: Verification and Testing, 2012

Latent fault detection in large scale services.
Proceedings of the IEEE/IFIP International Conference on Dependable Systems and Networks, 2012

Anatomy of Alternating Quantifier Satisfiability (Work in progress).
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Program Verification as Satisfiability Modulo Theories.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

SMT-LIB Sequences and Regular Expressions.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Taking Satisfiability to the Next Level with Z3 - (Abstract).
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

From Primal Infon Logic with Individual Variables to Datalog.
Proceedings of the Correct Reasoning, 2012

2011
Foundations of Finite Symbolic Tree Transducers.
Bull. EATCS, 2011

Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272).
Dagstuhl Reports, 2011

Satisfiability modulo theories: introduction and applications.
Commun. ACM, 2011

Canonical Regular Types.
Proceedings of the Technical Communications of the 27th International Conference on Logic Programming, 2011

Symbolic Tree Transducers.
Proceedings of the Perspectives of Systems Informatics, 2011

<i>μZ</i>- An Efficient Engine for Fixed Points with Constraints.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010
Content-dependent chunking for differential compression, the local maximum approach.
J. Comput. Syst. Sci., 2010

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets.
J. Autom. Reason., 2010

Symbolic Automata Constraint Solving.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware.
Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware.
Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

Applications and Challenges in Satisfiability Modulo Theories.
Proceedings of the Second International Workshop on Invariant Generation, 2010

Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Linear Quantifier Elimination as an Abstract Decision Procedure.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

DKAL and Z3: A Logic Embedding Experiment.
Proceedings of the Fields of Logic and Computation, 2010

2009
Symbolic Bounded Model Checking of Abstract State Machines.
Int. J. Softw. Informatics, 2009

Path Feasibility Analysis for String-Manipulating Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

SMT Solvers for Testing, Program Analysis and Verification at Microsoft.
Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

Specifying and Composing Non-functional Requirements in Model-Based Development.
Proceedings of the Software Composition - 8th International Conference, 2009

Satisfiability Modulo Theories: An Appetizer.
Proceedings of the Formal Methods: Foundations and Applications, 2009

Input-Output Model Programs.
Proceedings of the Theoretical Aspects of Computing, 2009

Tapas: Theory Combinations and Practical Applications.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2009

Generalized, efficient array decision procedures.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Symbolic Bounded Conformance Checking of Model Programs.
Proceedings of the Perspectives of Systems Informatics, 2009

Linear Functional Fixed-points.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Modular difference logic is hard
CoRR, 2008

Z3: An Efficient SMT Solver.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Using Dynamic Symbolic Execution to Improve Deductive Verification.
Proceedings of the Model Checking Software, 2008

Proofs and Refutations, and Z3.
Proceedings of the LPAR 2008 Workshops, 2008

An SMT Approach to Bounded Reachability Analysis of Model Programs.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008

Engineering DPLL(T) + Saturation.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Model-based Theory Combination.
Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, 2007

Efficient E-Matching for SMT Solvers.
Proceedings of the Automated Deduction, 2007

Models and Software Model Checking of a Distributed File Replication System.
Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2001
Deductive verification of real-time systems using STeP.
Theor. Comput. Sci., 2001

2000
Verifying Temporal Properties of Reactive Systems: A STeP Tutorial.
Formal Methods Syst. Des., 2000

Absolute Explicit Unification.
Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

1998
Integrating decision procedures for temporal verification.
PhD thesis, 1998

An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems.
Proceedings of the International Workshop Tool Support for System Specification, 1998

Deciding Fixed and Non-fixed Size Bit-vectors.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

1997
Automatic Generation of Invariants and Intermediate Assertions.
Theor. Comput. Sci., 1997

A Practical Integration of First-Order Reasoning and Decision Procedures.
Proceedings of the Automated Deduction, 1997

1996
STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995
STeP: The Stanford Temporal Prover.
Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Automatic Generation of Invariants and Assertions.
Proceedings of the Principles and Practice of Constraint Programming, 1995


  Loading...