Stop the war!

Остановите войну!

for scientists:

default search action

combined dblp search
author search
venue search
publication search

ask others

Nikolaj S. Bjørner

> Home > Persons

Person information

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

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

Books and Theses

see FAQ

What is the meaning of the colors in the publication lists?

1998
[b1]
- view
  - electronic edition @ stanford.edu
  - no references & citations available
- export record
  dblp key:
  - phd/us/Bjorner98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/phd/us/Bjorner98
Nikolaj S. Bjørner:
Integrating decision procedures for temporal verification. Stanford University, USA, 1998

Journal Articles

see FAQ

What is the meaning of the colors in the publication lists?

2022
[j19]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/fac/HumenbergerABK22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fac/HumenbergerABK22
Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács:
Algebra-Based Reasoning for Loop Synthesis. Formal Aspects Comput. 34(1): 1-31 (2022)
2021
[j18]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/BjornerG21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/BjornerG21
Nikolaj S. Bjørner, Arie Gurfinkel:
Preface of the special issue on the conference on formal methods in computer aided design 2018. Formal Methods Syst. Des. 57(2): 119-120 (2021)
2018
[j17]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/acta/BoerB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/acta/BoerB18
Frank S. de Boer, Nikolaj S. Bjørner:
Preface for the special issue "FM15". Acta Informatica 55(6): 459-460 (2018)
[j16]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/fac/BjornerBB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fac/BjornerBB18
Nikolaj S. Bjørner, Frank S. de Boer, Andrew Butterfield:
Editorial. Formal Aspects Comput. 30(5): 493-494 (2018)
2017
[j15]
- view
  authority control:
- export record
  dblp key:
  - journals/ccr/BjornerCS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ccr/BjornerCS17
Nikolaj S. Bjørner, Marco Canini, Nik Sultana:
Report on Networking and Programming Languages 2017. Comput. Commun. Rev. 47(5): 39-41 (2017)
[j14]
- view
  authority control:
- export record
  dblp key:
  - journals/jacm/KarbyshevBIRS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jacm/KarbyshevBIRS17
Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham:
Property-Directed Inference of Universal Invariants or Proving Their Absence. J. ACM 64(1): 7:1-7:33 (2017)
[j13]
- view
  authority control:
- export record
  dblp key:
  - journals/jacm/VeanesBNB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jacm/VeanesBNB17
Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg:
Monadic Decomposition. J. ACM 64(2): 14:1-14:28 (2017)
2015
[j12]
- view
  authority control:
- export record
  dblp key:
  - journals/ipl/VeanesB15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ipl/VeanesB15
Margus Veanes, Nikolaj S. Bjørner:
Symbolic tree automata. Inf. Process. Lett. 115(3): 418-424 (2015)
2013
[j11]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BjornerS13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BjornerS13
Nikolaj S. Bjørner, Viorica Sofronie-Stokkermans:
Preface: Special Issue of Selected Extended Papers of CADE-23. J. Autom. Reason. 51(1): 1-2 (2013)
2012
[j10]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jsc/BjornerK12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jsc/BjornerK12
Nikolaj S. Bjørner, Laura Kovács:
Foreword. J. Symb. Comput. 47(12): 1413-1415 (2012)
[j9]
- view
  authority control:
- export record
  dblp key:
  - journals/sttt/VeanesB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sttt/VeanesB12
Margus Veanes, Nikolaj S. Bjørner:
Alternating simulation and IOCO. Int. J. Softw. Tools Technol. Transf. 14(4): 387-405 (2012)
2011
[j8]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/MouraB11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/MouraB11
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9): 69-77 (2011)
[j7]
- view
  - electronic edition @ eatcs.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/eatcs/VeanesB11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/eatcs/VeanesB11
Margus Veanes, Nikolaj S. Bjørner:
Foundations of Finite Symbolic Tree Transducers. Bull. EATCS 105: 141-173 (2011)
2010
[j6]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/PiskacMB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/PiskacMB10
Ruzica Piskac, Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reason. 44(4): 401-424 (2010)
[j5]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jcss/BjornerBG10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jcss/BjornerBG10
Nikolaj S. Bjørner, Andreas Blass, Yuri Gurevich:
Content-dependent chunking for differential compression, the local maximum approach. J. Comput. Syst. Sci. 76(3-4): 154-203 (2010)
2009
[j4]
- view
  - electronic edition @ ijsi.org
  - no references & citations available
- export record
  dblp key:
  - journals/ijsi/VeanesBGS09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ijsi/VeanesBGS09
Margus Veanes, Nikolaj S. Bjørner, Yuri Gurevich, Wolfram Schulte:
Symbolic Bounded Model Checking of Abstract State Machines. Int. J. Softw. Informatics 3(2-3): 149-170 (2009)
2001
[j3]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/tcs/BjornerMSU01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tcs/BjornerMSU01
Nikolaj S. Bjørner, Zohar Manna, Henny Sipma, Tomás E. Uribe:
Deductive verification of real-time systems using STeP. Theor. Comput. Sci. 253(1): 27-60 (2001)
2000
[j2]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/BjornerBCFMSU00
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/BjornerBCFMSU00
Nikolaj S. Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomás E. Uribe:
Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods Syst. Des. 16(3): 227-270 (2000)
1997
[j1]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/tcs/BjornerBM97
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tcs/BjornerBM97
Nikolaj S. Bjørner, Anca Browne, Zohar Manna:
Automatic Generation of Invariants and Intermediate Assertions. Theor. Comput. Sci. 173(1): 49-87 (1997)

Conference and Workshop Papers

see FAQ

What is the meaning of the colors in the publication lists?

2023
[c104]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BjornerF23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BjornerF23
Nikolaj S. Bjørner, Katalin Fazekas:
On Incremental Pre-processing for SMT. CADE 2023: 41-60
[c103]
- view
  authority control:
- export record
  dblp key:
  - conf/dac/LinKTBC23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dac/LinKTBC23
Wan-Hsuan Lin, Jason Kimko, Bochen Tan, Nikolaj S. Bjørner, Jason Cong:
Scalable Optimal Layout Synthesis for NISQ Quantum Processors. DAC 2023: 1-6
[c102]
- view
  - electronic edition @ usenix.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/nsdi/KrishnaswamySMB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nsdi/KrishnaswamySMB23
Umesh Krishnaswamy, Rachee Singh, Paul Mattes, Paul-Andre C. Bissonnette, Nikolaj S. Bjørner, Zahira Nasrin, Sonal Kothari, Prabhakar Reddy, John Abeln, Srikanth Kandula, Himanshu Raj, Luis Irún-Briz, Jamie Gaudette, Erica Lan:
OneWAN is better than two: Unifying a split WAN architecture. NSDI 2023: 515-529
[c101]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/BjornerEK23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/BjornerEK23
Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács:
Satisfiability Modulo Custom Theories in Z3. VMCAI 2023: 91-105
2022
[c100]
- view
  - electronic edition @ usenix.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/nsdi/KrishnaswamySBR22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nsdi/KrishnaswamySBR22
Umesh Krishnaswamy, Rachee Singh, Nikolaj S. Bjørner, Himanshu Raj:
Decentralized cloud wide-area network traffic engineering with BLASTSHIELD. NSDI 2022: 325-338
[c99]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/sat/NarodytskaB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/NarodytskaB22
Nina Narodytska, Nikolaj S. Bjørner:
Analysis of Core-Guided MaxSat Using Cores and Correction Sets. SAT 2022: 26:1-26:20
[c98]
- view
  - electronic edition @ ceur-ws.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/smt/BjornerEK22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/BjornerEK22
Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács:
User-Propagators for Custom Theories in SMT Solving. SMT 2022: 71-79
[c97]
- view
  authority control:
- export record
  dblp key:
  - conf/sosr/SinghBK22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sosr/SinghBK22
Rachee Singh, Nikolaj S. Bjørner, Umesh Krishnaswamy:
Traffic engineering: from ISP to cloud wide area networks. SOSR 2022: 50-58
2021
[c96]
- view
  authority control:
- export record
  dblp key:
  - conf/cpaior/BjornerLLRV21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpaior/BjornerLLRV21
Nikolaj S. Bjørner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati:
Supercharging Plant Configurations Using Z3. CPAIOR 2021: 1-25
[c95]
- view
  authority control:
- export record
  dblp key:
  - conf/pldi/StanfordVB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pldi/StanfordVB21
Caleb Stanford, Margus Veanes, Nikolaj S. Bjørner:
Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. PLDI 2021: 620-635
[c94]
- view
  authority control:
- export record
  dblp key:
  - conf/sigcomm/SinghBSYAG21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigcomm/SinghBSYAG21
Rachee Singh, Nikolaj S. Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette:
Cost-effective capacity provisioning in wide area networks with Shoofly. SIGCOMM 2021: 534-546
2020
[c93]
- view
  authority control:
- export record
  dblp key:
  - conf/ifm/HumenbergerBK20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ifm/HumenbergerBK20
Andreas Humenberger, Nikolaj S. Bjørner, Laura Kovács:
Algebra-Based Loop Synthesis. IFM 2020: 440-459
[c92]
- view
  authority control:
- export record
  dblp key:
  - conf/sbmf/BjornerN20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sbmf/BjornerN20
Nikolaj S. Bjørner, Lev Nachmanson:
Navigating the Universe of Z3 Theory Solvers. SBMF 2020: 8-24
[c91]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/LevatichBPS20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/LevatichBPS20
Maxwell Levatich, Nikolaj S. Bjørner, Ruzica Piskac, Sharon Shoham:
Solving $\mathrm {LIA} ^\star $ Using Approximations. VMCAI 2020: 360-378
2019
[c90]
- view
  authority control:
- export record
  dblp key:
  - conf/date/MeuliSRBM19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/date/MeuliSRBM19
Giulia Meuli, Mathias Soeken, Martin Roetteler, Nikolaj S. Bjørner, Giovanni De Micheli:
Reversible Pebbling Game for Quantum Memory Management. DATE 2019: 288-291
[c89]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/SelsamB19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/SelsamB19
Daniel Selsam, Nikolaj S. Bjørner:
Guiding High-Performance SAT Solvers with Unsat-Core Predictions. SAT 2019: 336-353
[c88]
- view
  authority control:
- export record
  dblp key:
  - conf/sigcomm/BogleBGMBVS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigcomm/BogleBGMBVS19
Jeremy Bogle, Nikhil Bhatia, Manya Ghobadi, Ishai Menache, Nikolaj S. Bjørner, Asaf Valadarsky, Michael Schapira:
TEAVAR: striking the right utilization-availability balance in WAN traffic engineering. SIGCOMM 2019: 29-43
[c87]
- view
  authority control:
- export record
  dblp key:
  - conf/sigcomm/JayaramanBPABBF19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigcomm/JayaramanBPABBF19
Karthick Jayaraman, Nikolaj S. Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C. Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, Parag Sharma:
Validating datacenters at scale. SIGCOMM 2019: 200-213
[c86]
- view
  authority control:
- export record
  dblp key:
  - conf/synasc/GurfinkelB19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/synasc/GurfinkelB19
Arie Gurfinkel, Nikolaj S. Bjørner:
The Science, Art, and Magic of Constrained Horn Clauses. SYNASC 2019: 6-10
2018
[c85]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/Bjorner18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/Bjorner18
Nikolaj S. Bjørner:
Z3 and SMT in Industrial R&D. FM 2018: 675-678
[c84]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/ijcai/NarodytskaBMS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ijcai/NarodytskaBMS18
Nina Narodytska, Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv:
Core-Guided Minimal Correction Set and Core Enumeration. IJCAI 2018: 1353-1361
[c83]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/KorneevNPTBS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/KorneevNPTBS18
Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv:
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. SAT 2018: 438-449
[c82]
- view
  authority control:
- export record
  dblp key:
  - conf/setss/BjornerMNW18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/setss/BjornerMNW18
Nikolaj S. Bjørner, Leonardo de Moura, Lev Nachmanson, Christoph M. Wintersteiger:
Programming Z3. SETSS 2018: 148-201
2017
[c81]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/gcai/BjornerMS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/gcai/BjornerMS17
Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv:
Abduction for Learning Smart City Rules. GCAI 2017: 233-238
[c80]
- view
  authority control:
- export record
  dblp key:
  - conf/icse/ShiTLBC17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icse/ShiTLBC17
August Shi, Suresh Thummalapenta, Shuvendu K. Lahiri, Nikolaj S. Bjørner, Jacek Czerwonka:
Optimizing test placement for module-level regression testing. ICSE 2017: 689-699
[c79]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/BjornerJLRS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BjornerJLRS17
Nikolaj S. Bjørner, Dejan Jovanovic, Tancrède Lepoint, Philipp Rümmer, Martin Schäf:
Abduction by Non-Experts. LPAR (Short Presentations) 2017: 58-72
[c78]
- view
  - electronic edition @ usenix.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/nsdi/RyzhykBCJSTV17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nsdi/RyzhykBCJSTV17
Leonid Ryzhyk, Nikolaj S. Bjørner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, George Varghese:
Correct by Construction Networks Using Stepwise Refinement. NSDI 2017: 683-698
2016
[c77]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/gcai/RegerB0V16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/gcai/RegerB0V16
Giles Reger, Nikolaj S. Bjørner, Martin Suda, Andrei Voronkov:
AVATAR Modulo Theories. GCAI 2016: 39-52
[c76]
- view
  authority control:
- export record
  dblp key:
  - conf/hvc/BjornerJMSV16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/hvc/BjornerJMSV16
Nikolaj S. Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese:
ddNF: An Efficient Data Structure for Header Spaces. Haifa Verification Conference 2016: 49-64
[c75]
- view
  authority control:
- export record
  dblp key:
  - conf/pldi/GleissenthallBR16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pldi/GleissenthallBR16
Klaus von Gleissenthall, Nikolaj S. Bjørner, Andrey Rybalchenko:
Cardinalities and universal quantifiers for verifying parameterized systems. PLDI 2016: 599-613
[c74]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/PlotkinBLRV16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/PlotkinBLRV16
Gordon D. Plotkin, Nikolaj S. Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese:
Scaling network verification using symmetry and surgery. POPL 2016: 69-83
2015
[c73]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/BjornerGMR15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/BjornerGMR15
Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko:
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II 2015: 24-51
[c72]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cav/KarbyshevBIRS15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/KarbyshevBIRS15
Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham:
Property-Directed Inference of Universal Invariants or Proving Their Absence. CAV (1) 2015: 583-602
[c71]
- view
  authority control:
- export record
  dblp key:
  - conf/ershov/VeanesB15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ershov/VeanesB15
Margus Veanes, Nikolaj S. Bjørner:
Equivalence of Finite-Valued Symbolic Finite Transducers. Ershov Memorial Conference 2015: 276-290
[c70]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/KomuravelliBGM15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/KomuravelliBGM15
Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96
[c69]
- view
  authority control:
- export record
  dblp key:
  - conf/icdcit/BjornerJ15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icdcit/BjornerJ15
Nikolaj S. Bjørner, Karthick Jayaraman:
Checking Cloud Contracts in Microsoft Azure. ICDCIT 2015: 21-32
[c68]
- view
  - electronic edition @ ijcai.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/ijcai/BjornerN15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ijcai/BjornerN15
Nikolaj S. Bjørner, Nina Narodytska:
Maximum Satisfiability Using Cores and Correction Sets. IJCAI 2015: 246-252
[c67]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/BjornerJ15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BjornerJ15
Nikolaj S. Bjørner, Mikolás Janota:
Playing with Quantified Satisfaction. LPAR (short papers) 2015: 15-27
[c66]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/BjornerJK15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BjornerJK15
Nikolaj S. Bjørner, Mikolás Janota, William Klieber:
On Conflicts and Strategies in QBF. LPAR (short papers) 2015: 28-41
[c65]
- view
  - electronic edition @ usenix.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/nsdi/LopesBGJV15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nsdi/LopesBGJV15
Nuno P. Lopes, Nikolaj S. Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese:
Checking Beliefs in Dynamic Networks. NSDI 2015: 499-512
[c64]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/BjornerPF15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/BjornerPF15
Nikolaj S. Bjørner, Anh-Dung Phan, Lars Fleckenstein:
νZ - An Optimizing SMT Solver. TACAS 2015: 194-199
[c63]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/BjornerG15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/BjornerG15
Nikolaj S. Bjørner, Arie Gurfinkel:
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281
2014
[c62]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BerdineB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BerdineB14
Josh Berdine, Nikolaj S. Bjørner:
Computing All Implied Equalities via SMT-Based Partition Refinement. IJCAR 2014: 168-183
[c61]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cav/ItzhakyBRST14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/ItzhakyBRST14
Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur:
Property-Directed Shape Analysis. CAV 2014: 35-51
[c60]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cav/VeanesBNB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/VeanesBNB14
Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg:
Monadic Decomposition. CAV 2014: 628-645
[c59]
- view
  authority control:
- export record
  dblp key:
  - conf/icse/VisserBS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icse/VisserBS14
Willem Visser, Nikolaj S. Bjørner, Natarajan Shankar:
Software engineering and automated deduction. FOSE 2014: 155-166
[c58]
- view
  authority control:
- export record
  dblp key:
  - conf/pldi/BallBGIKSSV14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pldi/BallBGIKSSV14
Thomas Ball, Nikolaj S. Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky:
VeriCon: towards verifying controller programs in software-defined networks. PLDI 2014: 282-293
[c57]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/sycss/BjornerP14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sycss/BjornerP14
Nikolaj S. Bjørner, Anh-Dung Phan:
νZ - Maximal Satisfaction with Z3. SCSS 2014: 1-9
2013
[c56]
- view
  - electronic edition @ aaai.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/flairs/HowardJCCB13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/flairs/HowardJCCB13
Ayanna M. Howard, David Johnson, Cristina Conati, Frederick W. Chen, Nikolaj S. Bjørner:
Invited Talk Abstracts. FLAIRS 2013
[c55]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/BjornerGKL13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BjornerGKL13
Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav:
Instantiations, Zippers and EPR Interpolation. LPAR (short papers) 2013: 35-41
[c54]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/VeanesBNB13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/VeanesBNB13
Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg:
Effectively Monadic Predicates. LPAR (short papers) 2013: 97-103
[c53]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/BerdineBIKW13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BerdineBIKW13
Josh Berdine, Nikolaj S. Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger:
Resourceful Reachability as HORN-LA. LPAR 2013: 137-146
[c52]
- view
  authority control:
- export record
  dblp key:
  - conf/sas/BjornerMR13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sas/BjornerMR13
Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
On Solving Universally Quantified Horn Clauses. SAS 2013: 105-125
[c51]
- view
  authority control:
- export record
  dblp key:
  - conf/sigada/Bjorner13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigada/Bjorner13
Nikolaj S. Bjørner:
Satisfiability modulo theories for high integrity development. HILT 2013: 5-6
2012
[c50]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/BjornerCG12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/BjornerCG12
Nikolaj S. Bjørner, Guido de Caso, Yuri Gurevich:
From Primal Infon Logic with Individual Variables to Datalog. Correct Reasoning 2012: 72-86
[c49]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/Bjorner12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/Bjorner12
Nikolaj S. Bjørner:
Taking Satisfiability to the Next Level with Z3 - (Abstract). IJCAR 2012: 1-8
[c48]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BjornerMR12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BjornerMR12
Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Program Verification as Satisfiability Modulo Theories. SMT@IJCAR 2012: 3-11
[c47]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BjornerGMV12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BjornerGMV12
Nikolaj S. Bjørner, Vijay Ganesh, Raphaël Michel, Margus Veanes:
SMT-LIB Sequences and Regular Expressions. SMT@IJCAR 2012: 77-87
[c46]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/PhanBM12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/PhanBM12
Anh-Dung Phan, Nikolaj S. Bjørner, David Monniaux:
Anatomy of Alternating Quantifier Satisfiability (Work in progress). SMT@IJCAR 2012: 120-130
[c45]
- view
  authority control:
- export record
  dblp key:
  - conf/dsn/GabelSBB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dsn/GabelSBB12
Moshe Gabel, Assaf Schuster, Ran Gilad-Bachrach, Nikolaj S. Bjørner:
Latent fault detection in large scale services. DSN 2012: 1-12
[c44]
- view
  authority control:
- export record
  dblp key:
  - conf/hvc/Bjorner12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/hvc/Bjorner12
Nikolaj S. Bjørner:
SMT in Verification, Modeling, and Testing at Microsoft. Haifa Verification Conference 2012: 3
[c43]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/Bjorner12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/Bjorner12
Nikolaj S. Bjørner:
Engineering Theories with Z3. IWIL@LPAR 2012: 1-2
[c42]
- view
  authority control:
- export record
  dblp key:
  - conf/models/JacksonSB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/models/JacksonSB12
Ethan K. Jackson, Wolfram Schulte, Nikolaj S. Bjørner:
Detecting Specification Errors in Declarative Languages with Constraints. MoDELS 2012: 399-414
[c41]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/VeanesHLMB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/VeanesHLMB12
Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj S. Bjørner:
Symbolic finite state transducers: algorithms and applications. POPL 2012: 137-150
[c40]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/HoderB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/HoderB12
Krystof Hoder, Nikolaj S. Bjørner:
Generalized Property Directed Reachability. SAT 2012: 157-171
[c39]
- view
  authority control:
- export record
  dblp key:
  - conf/spin/BallBMMV12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/spin/BallBMMV12
Thomas Ball, Nikolaj S. Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes:
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN 2012: 1-6
[c38]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/VeanesB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/VeanesB12
Margus Veanes, Nikolaj S. Bjørner:
Symbolic Automata: The Toolkit. TACAS 2012: 472-477
2011
[c37]
- view
  authority control:
- export record
  dblp key:
  - conf/aplas/Bjorner11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/aplas/Bjorner11
Nikolaj S. Bjørner:
Engineering Theories with Z3. APLAS 2011: 4-16
[c36]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cav/HoderBM11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/HoderBM11
Krystof Hoder, Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
μZ- An Efficient Engine for Fixed Points with Constraints. CAV 2011: 457-462
[c35]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Bjorner11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Bjorner11
Nikolaj S. Bjørner:
Engineering Theories with Z3. CPP 2011: 1-2
[c34]
- view
  authority control:
- export record
  dblp key:
  - conf/ershov/VeanesB11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ershov/VeanesB11
Margus Veanes, Nikolaj S. Bjørner:
Symbolic Tree Transducers. Ershov Memorial Conference 2011: 377-393
[c33]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/iclp/JacksonBS11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/iclp/JacksonBS11
Ethan K. Jackson, Nikolaj S. Bjørner, Wolfram Schulte:
Canonical Regular Types. ICLP (Technical Communications) 2011: 73-83
2010
[c32]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/MeraB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/MeraB10
Sergio Mera, Nikolaj S. Bjørner:
DKAL and Z3: A Logic Embedding Experiment. Fields of Logic and Computation 2010: 504-528
[c31]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/MouraB10a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/MouraB10a
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Applications and Challenges in Satisfiability Modulo Theories. WING@ETAPS/IJCAR 2010: 1-11
[c30]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/Bjorner10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/Bjorner10
Nikolaj S. Bjørner:
Linear Quantifier Elimination as an Abstract Decision Procedure. IJCAR 2010: 316-330
[c29]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/MouraB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/MouraB10
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. IJCAR 2010: 400-411
[c28]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/VeanesBM10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/VeanesBM10
Margus Veanes, Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Symbolic Automata Constraint Solving. LPAR (Yogyakarta) 2010: 640-654
[c27]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/pts/VeanesB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pts/VeanesB10
Margus Veanes, Nikolaj S. Bjørner:
Alternating Simulation and IOCO. ICTSS 2010: 47-62
2009
[c26]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cav/BjornerH09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BjornerH09
Nikolaj S. Bjørner, Joe Hendrix:
Linear Functional Fixed-points. CAV 2009: 124-139
[c25]
- view
  authority control:
- export record
  dblp key:
  - conf/ershov/VeanesB09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ershov/VeanesB09
Margus Veanes, Nikolaj S. Bjørner:
Symbolic Bounded Conformance Checking of Model Programs. Ershov Memorial Conference 2009: 388-400
[c24]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/MouraB09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/MouraB09
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Generalized, efficient array decision procedures. FMCAD 2009: 45-52
[c23]
- view
  authority control:
- export record
  dblp key:
  - conf/formats/BjornerM09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/formats/BjornerM09
Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Tapas: Theory Combinations and Practical Applications. FORMATS 2009: 1-6
[c22]
- view
  authority control:
- export record
  dblp key:
  - conf/ictac/VeanesB09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ictac/VeanesB09
Margus Veanes, Nikolaj S. Bjørner:
Input-Output Model Programs. ICTAC 2009: 322-335
[c21]
- view
  authority control:
- export record
  dblp key:
  - conf/sbmf/MouraB09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sbmf/MouraB09
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Satisfiability Modulo Theories: An Appetizer. SBMF 2009: 23-36
[c20]
- view
  authority control:
- export record
  dblp key:
  - conf/soco/JacksonSDSBS09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/soco/JacksonSDSBS09
Ethan K. Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj S. Bjørner, Wolfram Schulte:
Specifying and Composing Non-functional Requirements in Model-Based Development. SC@TOOLS 2009: 72-89
[c19]
- view
  authority control:
- export record
  dblp key:
  - conf/synasc/Bjorner09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/synasc/Bjorner09
Nikolaj S. Bjørner:
SMT Solvers for Testing, Program Analysis and Verification at Microsoft. SYNASC 2009: 15
[c18]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/BjornerTV09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/BjornerTV09
Nikolaj S. Bjørner, Nikolai Tillmann, Andrei Voronkov:
Path Feasibility Analysis for String-Manipulating Programs. TACAS 2009: 307-321
2008
[c17]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/MouraB08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/MouraB08
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. IJCAR 2008: 410-425
[c16]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/MouraB08a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/MouraB08a
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Engineering DPLL(T) + Saturation. IJCAR 2008: 475-490
[c15]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/forte/VeanesBR08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/forte/VeanesBR08
Margus Veanes, Nikolaj S. Bjørner, Alexander Raschke:
An SMT Approach to Bounded Reachability Analysis of Model Programs. FORTE 2008: 53-68
[c14]
- view
  - electronic edition @ ceur-ws.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/lpar/MouraB08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/MouraB08
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Proofs and Refutations, and Z3. LPAR Workshops 2008
[c13]
- view
  authority control:
- export record
  dblp key:
  - conf/spin/VanoverbergheBHST08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/spin/VanoverbergheBHST08
Dries Vanoverberghe, Nikolaj S. Bjørner, Jonathan de Halleux, Wolfram Schulte, Nikolai Tillmann:
Using Dynamic Symbolic Execution to Improve Deductive Verification. SPIN 2008: 9-25
[c12]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/MouraB08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/MouraB08
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Z3: An Efficient SMT Solver. TACAS 2008: 337-340
2007
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/Bjorner07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/Bjorner07
Nikolaj S. Bjørner:
Models and Software Model Checking of a Distributed File Replication System. Formal Methods and Hybrid Real-Time Systems 2007: 1-23
[c10]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/MouraB07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/MouraB07
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Efficient E-Matching for SMT Solvers. CADE 2007: 183-198
[c9]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/MouraB08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/MouraB08
Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Model-based Theory Combination. SMT@CAV 2007: 37-49
2000
[c8]
- view
  authority control:
- export record
  dblp key:
  - conf/rta/BjornerM00
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/rta/BjornerM00
Nikolaj S. Bjørner, César A. Muñoz:
Absolute Explicit Unification. RTA 2000: 31-46
1998
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/BjornerP98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/BjornerP98
Nikolaj S. Bjørner, Mark C. Pichora:
Deciding Fixed and Non-fixed Size Bit-vectors. TACAS 1998: 376-392
[c6]
- view
  authority control:
- export record
  dblp key:
  - conf/tssdv/MannaBBCFPSU98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tssdv/MannaBBCFPSU98
Zohar Manna, Nikolaj S. Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Mark C. Pichora, Henny B. Sipma, Tomás E. Uribe:
An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. Tool Support for System Specification, Development and Verification 1998: 174-188
1997
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/arts/BjornerMSU97
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/arts/BjornerMSU97
Nikolaj S. Bjørner, Zohar Manna, Henny Sipma, Tomás E. Uribe:
Deductive Verification of Real-Time Systems Using STeP. ARTS 1997: 22-43
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BjornerSU97
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BjornerSU97
Nikolaj S. Bjørner, Mark E. Stickel, Tomás E. Uribe:
A Practical Integration of First-Order Reasoning and Decision Procedures. CADE 1997: 101-115
1996
[c3]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/BjornerBCCKMSU96
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BjornerBCCKMSU96
Nikolaj S. Bjørner, Anca Browne, Edward Y. Chang, Michael Colón, Arjun Kapur, Zohar Manna, Henny Sipma, Tomás E. Uribe:
STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. CAV 1996: 415-418
1995
[c2]
- view
  authority control:
- export record
  dblp key:
  - conf/cp/BjornerBM95
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cp/BjornerBM95
Nikolaj S. Bjørner, Anca Browne, Zohar Manna:
Automatic Generation of Invariants and Assertions. CP 1995: 589-623
[c1]
- view
  authority control:
- export record
  dblp key:
  - conf/tapsoft/MannaBBCCADKLSU95
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tapsoft/MannaBBCCADKLSU95
Zohar Manna, Nikolaj S. Bjørner, Anca Browne, Edward Y. Chang, Michael Colón, Luca de Alfaro, Harish Devarajan, Arjun Kapur, Jaejin Lee, Henny Sipma, Tomás E. Uribe:
STeP: The Stanford Temporal Prover. TAPSOFT 1995: 793-794

Parts in Books or Collections

see FAQ

What is the meaning of the colors in the publication lists?

2016
[p2]
- view
  authority control:
- export record
  dblp key:
  - series/natosec/Bjorner16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/series/natosec/Bjorner16
Nikolaj S. Bjørner:
SMT Solvers: Foundations and Applications. Dependable Software Systems Engineering 2016: 24-32
2014
[p1]
- view
  authority control:
- export record
  dblp key:
  - books/cu/p/BjornerM14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/books/cu/p/BjornerM14
Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Tractability and Modern Satisfiability Modulo Theories Solvers. Tractability 2014: 350-377

Editorship

see FAQ

What is the meaning of the colors in the publication lists?

2019
[e10]
- view
  authority control:
- export record
  dblp key:
  - conf/ershov/2019
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ershov/2019
Nikolaj S. Bjørner, Irina B. Virbitskaite, Andrei Voronkov:
Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Novosibirsk, Russia, July 2-5, 2019, Revised Selected Papers. Lecture Notes in Computer Science 11964, Springer 2019, ISBN 978-3-030-37486-0 [contents]
2018
[e9]
- view
- export record
  dblp key:
  - conf/fmcad/2018
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/2018
Nikolaj S. Bjørner, Arie Gurfinkel:
2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. IEEE 2018, ISBN 978-0-9835678-8-2 [contents]
2016
[e8]
- view
  authority control:
- export record
  dblp key:
  - conf/icdcit/2016
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icdcit/2016
Nikolaj S. Bjørner, Sanjiva Prasad, Laxmi Parida:
Distributed Computing and Internet Technology - 12th International Conference, ICDCIT 2016, Bhubaneswar, India, January 15-18, 2016, Proceedings. Lecture Notes in Computer Science 9581, Springer 2016, ISBN 978-3-319-28033-2 [contents]
2015
[e7]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/2015
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/2015
Nikolaj S. Bjørner, Frank S. de Boer:
FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. Lecture Notes in Computer Science 9109, Springer 2015, ISBN 978-3-319-19248-2 [contents]
2014
[e6]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/BjornerFRS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BjornerFRS14
Nikolaj S. Bjørner, Fabio Fioravanti, Andrey Rybalchenko, Valerio Senni:
Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014. EPTCS 169, 2014 [contents]
2013
[e5]
- view
- export record
  dblp key:
  - conf/synasc/2013
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/synasc/2013
Nikolaj S. Bjørner, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen M. Watt, Daniela Zaharie:
15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, September 23-26, 2013. IEEE Computer Society 2013, ISBN 978-1-4799-3035-7 [contents]
2012
[e4]
- view
- export record
  dblp key:
  - conf/cade/2010wing
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/2010wing
Andrei Voronkov, Laura Kovács, Nikolaj S. Bjørner:
Second International Workshop on Invariant Generation, WING 2009, York, UK, March 29, 2009 and Third International Workshop on Invariant Generation, WING 2010, Edinburgh, UK, July 21, 2010. EPiC Series in Computing 1, EasyChair 2012 [contents]
[e3]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/2012
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/2012
Nikolaj S. Bjørner, Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings. Lecture Notes in Computer Science 7180, Springer 2012, ISBN 978-3-642-28716-9 [contents]
2011
[e2]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/2011
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/2011
Nikolaj S. Bjørner, Viorica Sofronie-Stokkermans:
Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings. Lecture Notes in Computer Science 6803, Springer 2011, ISBN 978-3-642-22437-9 [contents]
2010
[e1]
- view
- export record
  dblp key:
  - conf/dagstuhl/2010P10161
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dagstuhl/2010P10161
Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov:
Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010. Dagstuhl Seminar Proceedings 10161, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany 2010 [contents]

Informal and Other Publications

see FAQ

What is the meaning of the colors in the publication lists?

2023
[i17]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2304-08655
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2304-08655
Nikolaj S. Bjørner, Shuo Chen, Yang Chen, Zhongxin Guo, Peng Liu, Nanqing Luo:
An Ethereum-compatible blockchain that explicates and ensures design-level safety properties for smart contracts. CoRR abs/2304.08655 (2023)
2022
[i16]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2206-11495
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2206-11495
Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács:
Algebra-Based Reasoning for Loop Synthesis. CoRR abs/2206.11495 (2022)
2021
[i15]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BjornerCMR21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BjornerCMR21
Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, Grigore Rosu:
Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). Dagstuhl Reports 11(9): 80-101 (2021)
2019
[i14]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/abs-1903-04671
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1903-04671
Daniel Selsam, Nikolaj S. Bjørner:
NeuroCore: Guiding High-Performance SAT Solvers with Unsat-Core Predictions. CoRR abs/1903.04671 (2019)
[i13]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/abs-1904-02121
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1904-02121
Giulia Meuli, Mathias Soeken, Martin Roetteler, Nikolaj S. Bjørner, Giovanni De Micheli:
Reversible Pebbling Game for Quantum Memory Management. CoRR abs/1904.02121 (2019)
[i12]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BardinBC19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BardinBC19
Sébastien Bardin, Nikolaj S. Bjørner, Cristian Cadar:
Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062). Dagstuhl Reports 9(2): 27-47 (2019)
2018
[i11]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/abs-1802-08795
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1802-08795
Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv:
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. CoRR abs/1802.08795 (2018)
2015
[i10]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/KomuravelliBGM15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/KomuravelliBGM15
Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR abs/1508.01288 (2015)
[i9]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BjornerFGZ15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BjornerFGZ15
Nikolaj S. Bjørner, Nate Foster, Philip Brighten Godfrey, Pamela Zave:
Formal Foundations for Networking (Dagstuhl Seminar 15071). Dagstuhl Reports 5(2): 44-63 (2015)
[i8]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BjornerBSW15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BjornerBSW15
Nikolaj S. Bjørner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, Christoph Weidenbach:
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). Dagstuhl Reports 5(9): 18-37 (2015)
2013
[i7]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/BjornerMR13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BjornerMR13
Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR abs/1306.5264 (2013)
[i6]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BjornerHNW13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BjornerHNW13
Nikolaj S. Bjørner, Reiner Hähnle, Tobias Nipkow, Christoph Weidenbach:
Deduction and Arithmetic (Dagstuhl Seminar 13411). Dagstuhl Reports 3(10): 1-24 (2013)
2012
[i5]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BjornerCKM12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BjornerCKM12
Nikolaj S. Bjørner, Krishnendu Chatterjee, Laura Kovács, Rupak Majumdar:
Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). Dagstuhl Reports 2(11): 45-65 (2012)
2011
[i4]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BjornerNVV11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BjornerNVV11
Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov:
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports 1(7): 23-35 (2011)
2010
[i3]
- view
  - electronic edition @ dagstuhl.de (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/dagstuhl/BjornerNVV10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dagstuhl/BjornerNVV10
Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov:
10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware 2010
[i2]
- view
  - electronic edition @ dagstuhl.de (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/dagstuhl/BjornerNVV10a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dagstuhl/BjornerNVV10a
Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov:
10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware 2010
2008
[i1]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/abs-0811-0987
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-0811-0987
Nikolaj S. Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi:
Modular difference logic is hard. CoRR abs/0811.0987 (2008)

Coauthor Index

see FAQ

a service of

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.