Nikolaj Bjørner

According to our database1, Nikolaj Bjørner
  • authored at least 108 papers between 1995 and 2018.
  • has a "Dijkstra number"2 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2018
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures.
CoRR, 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.
Computer Communication Review, 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

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays.
CoRR, 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

Property-Directed Inference of Universal Invariants or Proving Their Absence.
Proceedings of the Computer Aided Verification - 27th International Conference, 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

Monadic Decomposition.
Proceedings of the Computer Aided Verification - 26th International Conference, 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. Reasoning, 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.
STTT, 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.
Bulletin of the 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

Engineering Theories with Z3.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

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

Engineering Theories with Z3.
Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 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. Reasoning, 2010

Alternating Simulation and IOCO.
Proceedings of the Testing Software and Systems, 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. Software and 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, SC 2009, Zurich, 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
Model-based Theory Combination.
Electr. Notes Theor. Comput. Sci., 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
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 in System Design, 2000

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

1998
Deiding 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

Deductive Verification of Real-Time Systems Using STeP.
Proceedings of the Transformation-Based Reactive Systems Development, 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...