default search action
Nikolaj S. Bjørner
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
2020 – today
- 2024
- [j20]Avery Laird
, Bangtian Liu
SpEQ: Translation of Sparse Codes using Equivalences. Proc. ACM Program. Lang. 8(PLDI): 1680-1703 (2024) - [c106]Nikolaj S. Bjørner, Lev Nachmanson:
Arithmetic Solving in Z3. CAV (1) 2024: 26-41 - [c105]Abhishek Vijaya Kumar, Bill Owens, Nikolaj S. Bjørner, Binbin Guan, Yawei Yin, Paramvir Bahl, Rachee Singh:
CHISEL: An optical slice of the wide-area network. NSDI 2024: 859-875 - [e12]Nikolaj S. Bjørner, Marijn Heule, Andrei Voronkov:
LPAR 2024 Complementary Volume, Port Louis, Mauritius, May 26-31, 2024. Kalpa Publications in Computing 18, EasyChair 2024 [contents] - [e11]Nikolaj S. Bjørner, Marijn Heule, Andrei Voronkov:
LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024. EPiC Series in Computing 100, EasyChair 2024 [contents] - [i19]Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj S. Bjørner, Laura Kovács:
PolySAT: Word-level Bit-vector Reasoning in Z3. CoRR abs/2406.04696 (2024) - [i18]Nikolaj S. Bjørner, Ashley J. Chen, Shuo Chen, Yang Chen, Zhongxin Guo, Tzu-Han Hsu, Peng Liu, Nanqing Luo:
Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions. CoRR abs/2408.06478 (2024) - 2023
- [c104]Nikolaj S. Bjørner, Katalin Fazekas
On Incremental Pre-processing for SMT. CADE 2023: 41-60 - [c103]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]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]Nikolaj S. Bjørner
Satisfiability Modulo Custom Theories in Z3. VMCAI 2023: 91-105 - [i17]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
- [j19]Andreas Humenberger, Daneshvar Amrollahi
Algebra-Based Reasoning for Loop Synthesis. Formal Aspects Comput. 34(1): 1-31 (2022) - [c100]Umesh Krishnaswamy, Rachee Singh, Nikolaj S. Bjørner, Himanshu Raj:
Decentralized cloud wide-area network traffic engineering with BLASTSHIELD. NSDI 2022: 325-338 - [c99]Nina Narodytska, Nikolaj S. Bjørner:
Analysis of Core-Guided MaxSat Using Cores and Correction Sets. SAT 2022: 26:1-26:20 - [c98]Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács:
User-Propagators for Custom Theories in SMT Solving. SMT 2022: 71-79 - [c97]Rachee Singh, Nikolaj S. Bjørner, Umesh Krishnaswamy:
Traffic engineering: from ISP to cloud wide area networks. SOSR 2022: 50-58 - [i16]Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács:
Algebra-Based Reasoning for Loop Synthesis. CoRR abs/2206.11495 (2022) - 2021
- [j18]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) - [c96]Nikolaj S. Bjørner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati:
Supercharging Plant Configurations Using Z3. CPAIOR 2021: 1-25 - [c95]Caleb Stanford
Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. PLDI 2021: 620-635 - [c94]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 - [i15]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) - 2020
- [c93]Andreas Humenberger, Nikolaj S. Bjørner, Laura Kovács
Algebra-Based Loop Synthesis. IFM 2020: 440-459 - [c92]Nikolaj S. Bjørner, Lev Nachmanson:
Navigating the Universe of Z3 Theory Solvers. SBMF 2020: 8-24 - [c91]Maxwell Levatich, Nikolaj S. Bjørner, Ruzica Piskac
Solving $\mathrm {LIA} ^\star $ Using Approximations. VMCAI 2020: 360-378
2010 – 2019
- 2019
- [c90]Giulia Meuli, Mathias Soeken, Martin Roetteler
Reversible Pebbling Game for Quantum Memory Management. DATE 2019: 288-291 - [c89]Daniel Selsam, Nikolaj S. Bjørner:
Guiding High-Performance SAT Solvers with Unsat-Core Predictions. SAT 2019: 336-353 - [c88]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]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]Arie Gurfinkel
The Science, Art, and Magic of Constrained Horn Clauses. SYNASC 2019: 6-10 - [e10]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] - [i14]Daniel Selsam, Nikolaj S. Bjørner:
NeuroCore: Guiding High-Performance SAT Solvers with Unsat-Core Predictions. CoRR abs/1903.04671 (2019) - [i13]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]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
- [j17]Frank S. de Boer, Nikolaj S. Bjørner:
Preface for the special issue "FM15". Acta Informatica 55(6): 459-460 (2018) - [j16]Nikolaj S. Bjørner, Frank S. de Boer, Andrew Butterfield:
Editorial. Formal Aspects Comput. 30(5): 493-494 (2018) - [c85]Nikolaj S. Bjørner:
Z3 and SMT in Industrial R&D. FM 2018: 675-678 - [c84]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]Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. SAT 2018: 438-449 - [c82]Nikolaj S. Bjørner, Leonardo de Moura, Lev Nachmanson, Christoph M. Wintersteiger
Programming Z3. SETSS 2018: 148-201 - [e9]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] - [i11]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) - 2017
- [j15]Nikolaj S. Bjørner, Marco Canini
Report on Networking and Programming Languages 2017. Comput. Commun. Rev. 47(5): 39-41 (2017) - [j14]Aleksandr Karbyshev
Property-Directed Inference of Universal Invariants or Proving Their Absence. J. ACM 64(1): 7:1-7:33 (2017) - [j13]Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg
Monadic Decomposition. J. ACM 64(2): 14:1-14:28 (2017) - [c81]Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv:
Abduction for Learning Smart City Rules. GCAI 2017: 233-238 - [c80]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]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]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]Giles Reger, Nikolaj S. Bjørner, Martin Suda, Andrei Voronkov:
AVATAR Modulo Theories. GCAI 2016: 39-52 - [c76]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]Klaus von Gleissenthall, Nikolaj S. Bjørner, Andrey Rybalchenko:
Cardinalities and universal quantifiers for verifying parameterized systems. PLDI 2016: 599-613 - [c74]Gordon D. Plotkin, Nikolaj S. Bjørner, Nuno P. Lopes
Scaling network verification using symmetry and surgery. POPL 2016: 69-83 - [p2]Nikolaj S. Bjørner:
SMT Solvers: Foundations and Applications. Dependable Software Systems Engineering 2016: 24-32 - [e8]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
- [j12]Margus Veanes, Nikolaj S. Bjørner:
Symbolic tree automata. Inf. Process. Lett. 115(3): 418-424 (2015) - [c73]Nikolaj S. Bjørner, Arie Gurfinkel
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II 2015: 24-51 - [c72]Aleksandr Karbyshev
Property-Directed Inference of Universal Invariants or Proving Their Absence. CAV (1) 2015: 583-602 - [c71]Margus Veanes, Nikolaj S. Bjørner:
Equivalence of Finite-Valued Symbolic Finite Transducers. Ershov Memorial Conference 2015: 276-290 - [c70]Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96 - [c69]Nikolaj S. Bjørner, Karthick Jayaraman:
Checking Cloud Contracts in Microsoft Azure. ICDCIT 2015: 21-32 - [c68]Nikolaj S. Bjørner, Nina Narodytska:
Maximum Satisfiability Using Cores and Correction Sets. IJCAI 2015: 246-252 - [c67]Nikolaj S. Bjørner, Mikolás Janota
Playing with Quantified Satisfaction. LPAR (short papers) 2015: 15-27 - [c66]Nikolaj S. Bjørner, Mikolás Janota, William Klieber:
On Conflicts and Strategies in QBF. LPAR (short papers) 2015: 28-41 - [c65]Nuno P. Lopes, Nikolaj S. Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese:
Checking Beliefs in Dynamic Networks. NSDI 2015: 499-512 - [c64]Nikolaj S. Bjørner, Anh-Dung Phan, Lars Fleckenstein:
νZ - An Optimizing SMT Solver. TACAS 2015: 194-199 - [c63]Nikolaj S. Bjørner, Arie Gurfinkel
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281 - [e7]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] - [i10]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]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]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) - 2014
- [c62]Josh Berdine, Nikolaj S. Bjørner:
Computing All Implied Equalities via SMT-Based Partition Refinement. IJCAR 2014: 168-183 - [c61]Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur:
Property-Directed Shape Analysis. CAV 2014: 35-51 - [c60]Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg:
Monadic Decomposition. CAV 2014: 628-645 - [c59]Willem Visser, Nikolaj S. Bjørner, Natarajan Shankar:
Software engineering and automated deduction. FOSE 2014: 155-166 - [c58]Thomas Ball, Nikolaj S. Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev
VeriCon: towards verifying controller programs in software-defined networks. PLDI 2014: 282-293 - [c57]Nikolaj S. Bjørner, Anh-Dung Phan:
νZ - Maximal Satisfaction with Z3. SCSS 2014: 1-9 - [p1]Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Tractability and Modern Satisfiability Modulo Theories Solvers. Tractability 2014: 350-377 - [e6]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
- [j11]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) - [c56]Ayanna M. Howard, David Johnson, Cristina Conati, Frederick W. Chen, Nikolaj S. Bjørner:
Invited Talk Abstracts. FLAIRS 2013 - [c55]Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav:
Instantiations, Zippers and EPR Interpolation. LPAR (short papers) 2013: 35-41 - [c54]Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg:
Effectively Monadic Predicates. LPAR (short papers) 2013: 97-103 - [c53]Josh Berdine, Nikolaj S. Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger
Resourceful Reachability as HORN-LA. LPAR 2013: 137-146 - [c52]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
On Solving Universally Quantified Horn Clauses. SAS 2013: 105-125 - [c51]Nikolaj S. Bjørner:
Satisfiability modulo theories for high integrity development. HILT 2013: 5-6 - [e5]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] - [i7]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]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
- [j10]Nikolaj S. Bjørner, Laura Kovács
Foreword. J. Symb. Comput. 47(12): 1413-1415 (2012) - [j9]Margus Veanes, Nikolaj S. Bjørner:
Alternating simulation and IOCO. Int. J. Softw. Tools Technol. Transf. 14(4): 387-405 (2012) - [c50]Nikolaj S. Bjørner, Guido de Caso, Yuri Gurevich:
From Primal Infon Logic with Individual Variables to Datalog. Correct Reasoning 2012: 72-86 - [c49]Nikolaj S. Bjørner:
Taking Satisfiability to the Next Level with Z3 - (Abstract). IJCAR 2012: 1-8 - [c48]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Program Verification as Satisfiability Modulo Theories. SMT@IJCAR 2012: 3-11 - [c47]Nikolaj S. Bjørner, Vijay Ganesh, Raphaël Michel, Margus Veanes:
SMT-LIB Sequences and Regular Expressions. SMT@IJCAR 2012: 77-87 - [c46]Anh-Dung Phan, Nikolaj S. Bjørner, David Monniaux:
Anatomy of Alternating Quantifier Satisfiability (Work in progress). SMT@IJCAR 2012: 120-130 - [c45]Moshe Gabel, Assaf Schuster, Ran Gilad-Bachrach
Latent fault detection in large scale services. DSN 2012: 1-12 - [c44]Nikolaj S. Bjørner:
SMT in Verification, Modeling, and Testing at Microsoft. Haifa Verification Conference 2012: 3 - [c43]Nikolaj S. Bjørner:
Engineering Theories with Z3. IWIL@LPAR 2012: 1-2 - [c42]Ethan K. Jackson, Wolfram Schulte, Nikolaj S. Bjørner:
Detecting Specification Errors in Declarative Languages with Constraints. MoDELS 2012: 399-414 - [c41]Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj S. Bjørner:
Symbolic finite state transducers: algorithms and applications. POPL 2012: 137-150 - [c40]Krystof Hoder, Nikolaj S. Bjørner:
Generalized Property Directed Reachability. SAT 2012: 157-171 - [c39]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]Margus Veanes, Nikolaj S. Bjørner:
Symbolic Automata: The Toolkit. TACAS 2012: 472-477 - [e4]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]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] - [i5]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
- [j8]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9): 69-77 (2011) - [j7]Margus Veanes, Nikolaj S. Bjørner:
Foundations of Finite Symbolic Tree Transducers. Bull. EATCS 105: 141-173 (2011) - [c37]Nikolaj S. Bjørner:
Engineering Theories with Z3. APLAS 2011: 4-16 - [c36]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]Nikolaj S. Bjørner:
Engineering Theories with Z3. CPP 2011: 1-2 - [c34]Margus Veanes, Nikolaj S. Bjørner:
Symbolic Tree Transducers. Ershov Memorial Conference 2011: 377-393 - [c33]Ethan K. Jackson, Nikolaj S. Bjørner, Wolfram Schulte:
Canonical Regular Types. ICLP (Technical Communications) 2011: 73-83 - [e2]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] - [i4]Nikolaj S. Bjørner, Robert Nieuwenhuis
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports 1(7): 23-35 (2011) - 2010
- [j6]Ruzica Piskac
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reason. 44(4): 401-424 (2010) - [j5]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) - [c32]Sergio Mera, Nikolaj S. Bjørner:
DKAL and Z3: A Logic Embedding Experiment. Fields of Logic and Computation 2010: 504-528 - [c31]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Applications and Challenges in Satisfiability Modulo Theories. WING@ETAPS/IJCAR 2010: 1-11 - [c30]Nikolaj S. Bjørner:
Linear Quantifier Elimination as an Abstract Decision Procedure. IJCAR 2010: 316-330 - [c29]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. IJCAR 2010: 400-411 - [c28]Margus Veanes, Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Symbolic Automata Constraint Solving. LPAR (Yogyakarta) 2010: 640-654 - [c27]Margus Veanes, Nikolaj S. Bjørner:
Alternating Simulation and IOCO. ICTSS 2010: 47-62 - [e1]Nikolaj S. Bjørner, Robert Nieuwenhuis
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] - [i3]Nikolaj S. Bjørner, Robert Nieuwenhuis
10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware 2010 - [i2]Nikolaj S. Bjørner, Robert Nieuwenhuis
10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware 2010
2000 – 2009
- 2009
- [j4]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) - [c26]Nikolaj S. Bjørner, Joe Hendrix:
Linear Functional Fixed-points. CAV 2009: 124-139 - [c25]Margus Veanes, Nikolaj S. Bjørner:
Symbolic Bounded Conformance Checking of Model Programs. Ershov Memorial Conference 2009: 388-400 - [c24]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Generalized, efficient array decision procedures. FMCAD 2009: 45-52 - [c23]Nikolaj S. Bjørner, Leonardo Mendonça de Moura:
Tapas: Theory Combinations and Practical Applications. FORMATS 2009: 1-6 - [c22]Margus Veanes, Nikolaj S. Bjørner:
Input-Output Model Programs. ICTAC 2009: 322-335 - [c21]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Satisfiability Modulo Theories: An Appetizer. SBMF 2009: 23-36 - [c20]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]Nikolaj S. Bjørner:
SMT Solvers for Testing, Program Analysis and Verification at Microsoft. SYNASC 2009: 15 - [c18]Nikolaj S. Bjørner, Nikolai Tillmann, Andrei Voronkov:
Path Feasibility Analysis for String-Manipulating Programs. TACAS 2009: 307-321 - 2008
- [c17]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. IJCAR 2008: 410-425 - [c16]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Engineering DPLL(T) + Saturation. IJCAR 2008: 475-490 - [c15]Margus Veanes, Nikolaj S. Bjørner, Alexander Raschke:
An SMT Approach to Bounded Reachability Analysis of Model Programs. FORTE 2008: 53-68 - [c14]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Proofs and Refutations, and Z3. LPAR Workshops 2008 - [c13]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]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Z3: An Efficient SMT Solver. TACAS 2008: 337-340 - [i1]Nikolaj S. Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi:
Modular difference logic is hard. CoRR abs/0811.0987 (2008) - 2007
- [c11]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]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Efficient E-Matching for SMT Solvers. CADE 2007: 183-198 - [c9]Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Model-based Theory Combination. SMT@CAV 2007: 37-49 - 2001
- [j3]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]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) - [c8]Nikolaj S. Bjørner, César A. Muñoz:
Absolute Explicit Unification. RTA 2000: 31-46
1990 – 1999
- 1998
- [b1]Nikolaj S. Bjørner:
Integrating decision procedures for temporal verification. Stanford University, USA, 1998 - [c7]Nikolaj S. Bjørner, Mark C. Pichora:
Deciding Fixed and Non-fixed Size Bit-vectors. TACAS 1998: 376-392 - [c6]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
- [j1]Nikolaj S. Bjørner, Anca Browne, Zohar Manna:
Automatic Generation of Invariants and Intermediate Assertions. Theor. Comput. Sci. 173(1): 49-87 (1997) - [c5]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]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]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]Nikolaj S. Bjørner, Anca Browne, Zohar Manna:
Automatic Generation of Invariants and Assertions. CP 1995: 589-623 - [c1]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
Coauthor Index
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.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-25 23:44 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: