Nikolaj S. Bjrner
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
81
Venues
32
Active years
1995–2025
Best venue rank
A*
Where they publish
- ACADE13 papers
- BLPAR9 papers
- A*CAV7 papers
- NationalNSDI5 papers
- ATACAS5 papers
- ASAT4 papers
- BFMCAD3 papers
- BVMCAI3 papers
- A*PLDI3 papers
- A*SIGCOMM3 papers
- NationalSYNASC2 papers
- A*IJCAI2 papers
- A*ICSE2 papers
- A*POPL2 papers
- NationalHOTNETS1 paper
- BTABLEAUX1 paper
- A*DAC1 paper
- BCPAIOR1 paper
- BIFM1 paper
- ADATE1 paper
- BFM1 paper
- NationalICDCIT1 paper
- NationalFlAIRS1 paper
- BSAS1 paper
- ADSN1 paper
- AMODELS1 paper
- BAPLAS1 paper
- BCPP1 paper
- BICLP1 paper
- CICTAC1 paper
- CFORTE1 paper
- ACP1 paper
Papers
81 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | FMCAD | Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols. | Petra Hozzov, Nikolaj S. Bjrner |
| 2025 | HOTNETS | Tackling Ambiguity in User Intent for LLM-based Network Configuration Synthesis. | Rajdeep Mondal, Nikolaj S. Bjrner, Todd D. Millstein, Alan Tang, George Varghese |
| 2025 | TABLEAUX | On Solving String Equations via Powers and Parikh Images. | Clemens Eisenhofer, Theodor Seiser, Nikolaj S. Bjrner, Laura Kovcs |
| 2024 | CAV | Arithmetic Solving in Z3. | Nikolaj S. Bjrner, Lev Nachmanson |
| 2024 | NSDI | CHISEL: An optical slice of the wide-area network. | Abhishek Vijaya Kumar, Bill Owens, Nikolaj S. Bjrner, Binbin Guan, Yawei Yin, Paramvir Bahl, Rachee Singh |
| 2023 | CADE | On Incremental Pre-processing for SMT. | Nikolaj S. Bjrner, Katalin Fazekas |
| 2023 | DAC | Scalable Optimal Layout Synthesis for NISQ Quantum Processors. | Wan-Hsuan Lin, Jason Kimko, Bochen Tan, Nikolaj S. Bjrner, Jason Cong |
| 2023 | NSDI | OneWAN is better than two: Unifying a split WAN architecture. | Umesh Krishnaswamy, Rachee Singh, Paul Mattes, Paul-Andre C. Bissonnette, Nikolaj S. Bjrner, Zahira Nasrin, Sonal Kothari, Prabhakar Reddy, John Abeln, Srikanth Kandula, Himanshu Raj, Luis Irn-Briz, Jamie Gaudette, Erica Lan |
| 2023 | VMCAI | Satisfiability Modulo Custom Theories in Z3. | Nikolaj S. Bjrner, Clemens Eisenhofer, Laura Kovcs |
| 2022 | NSDI | Decentralized cloud wide-area network traffic engineering with BLASTSHIELD. | Umesh Krishnaswamy, Rachee Singh, Nikolaj S. Bjrner, Himanshu Raj |
| 2022 | SAT | Analysis of Core-Guided MaxSat Using Cores and Correction Sets. | Nina Narodytska, Nikolaj S. Bjrner |
| 2021 | CPAIOR | Supercharging Plant Configurations Using Z3. | Nikolaj S. Bjrner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati |
| 2021 | PLDI | Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. | Caleb Stanford, Margus Veanes, Nikolaj S. Bjrner |
| 2021 | SIGCOMM | Cost-effective capacity provisioning in wide area networks with Shoofly. | Rachee Singh, Nikolaj S. Bjrner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette |
| 2020 | IFM | Algebra-Based Loop Synthesis. | Andreas Humenberger, Nikolaj S. Bjrner, Laura Kovcs |
| 2020 | VMCAI | Solving $\mathrm {LIA} ^\star $ Using Approximations. | Maxwell Levatich, Nikolaj S. Bjrner, Ruzica Piskac, Sharon Shoham |
| 2019 | DATE | Reversible Pebbling Game for Quantum Memory Management. | Giulia Meuli, Mathias Soeken, Martin Roetteler, Nikolaj S. Bjrner, Giovanni De Micheli |
| 2019 | SIGCOMM | TEAVAR: striking the right utilization-availability balance in WAN traffic engineering. | Jeremy Bogle, Nikhil Bhatia, Manya Ghobadi, Ishai Menache, Nikolaj S. Bjrner, Asaf Valadarsky, Michael Schapira |
| 2019 | SIGCOMM | Validating datacenters at scale. | Karthick Jayaraman, Nikolaj S. Bjrner, 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 |
| 2019 | SAT | Guiding High-Performance SAT Solvers with Unsat-Core Predictions. | Daniel Selsam, Nikolaj S. Bjrner |
| 2019 | SYNASC | The Science, Art, and Magic of Constrained Horn Clauses. | Arie Gurfinkel, Nikolaj S. Bjrner |
| 2018 | FM | Z3 and SMT in Industrial R&D. | Nikolaj S. Bjrner |
| 2018 | IJCAI | Core-Guided Minimal Correction Set and Core Enumeration. | Nina Narodytska, Nikolaj S. Bjrner, Maria-Cristina V. Marinescu, Mooly Sagiv |
| 2018 | SAT | Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. | Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjrner, Mooly Sagiv |
| 2017 | ICSE | Optimizing test placement for module-level regression testing. | August Shi, Suresh Thummalapenta, Shuvendu K. Lahiri, Nikolaj S. Bjrner, Jacek Czerwonka |
| 2017 | LPAR | Abduction by Non-Experts. | Nikolaj S. Bjrner, Dejan Jovanovic, Tancrde Lepoint, Philipp Rmmer, Martin Schf |
| 2017 | NSDI | Correct by Construction Networks Using Stepwise Refinement. | Leonid Ryzhyk, Nikolaj S. Bjrner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, George Varghese |
| 2016 | PLDI | Cardinalities and universal quantifiers for verifying parameterized systems. | Klaus von Gleissenthall, Nikolaj S. Bjrner, Andrey Rybalchenko |
| 2016 | POPL | Scaling network verification using symmetry and surgery. | Gordon D. Plotkin, Nikolaj S. Bjrner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese |
| 2015 | CAV | Property-Directed Inference of Universal Invariants or Proving Their Absence. | Aleksandr Karbyshev, Nikolaj S. Bjrner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2015 | FMCAD | Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. | Anvesh Komuravelli, Nikolaj S. Bjrner, Arie Gurfinkel, Kenneth L. McMillan |
| 2015 | ICDCIT | Checking Cloud Contracts in Microsoft Azure. | Nikolaj S. Bjrner, Karthick Jayaraman |
| 2015 | IJCAI | Maximum Satisfiability Using Cores and Correction Sets. | Nikolaj S. Bjrner, Nina Narodytska |
| 2015 | LPAR | Playing with Quantified Satisfaction. | Nikolaj S. Bjrner, Mikols Janota |
| 2015 | LPAR | On Conflicts and Strategies in QBF. | Nikolaj S. Bjrner, Mikols Janota, William Klieber |
| 2015 | NSDI | Checking Beliefs in Dynamic Networks. | Nuno P. Lopes, Nikolaj S. Bjrner, Patrice Godefroid, Karthick Jayaraman, George Varghese |
| 2015 | TACAS | νZ - An Optimizing SMT Solver. | Nikolaj S. Bjrner, Anh-Dung Phan, Lars Fleckenstein |
| 2015 | VMCAI | Property Directed Polyhedral Abstraction. | Nikolaj S. Bjrner, Arie Gurfinkel |
| 2014 | CADE | Computing All Implied Equalities via SMT-Based Partition Refinement. | Josh Berdine, Nikolaj S. Bjrner |
| 2014 | CAV | Property-Directed Shape Analysis. | Shachar Itzhaky, Nikolaj S. Bjrner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur |
| 2014 | CAV | Monadic Decomposition. | Margus Veanes, Nikolaj S. Bjrner, Lev Nachmanson, Sergey Bereg |
| 2014 | ICSE | Software engineering and automated deduction. | Willem Visser, Nikolaj S. Bjrner, Natarajan Shankar |
| 2014 | PLDI | VeriCon: towards verifying controller programs in software-defined networks. | Thomas Ball, Nikolaj S. Bjrner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky |
| 2013 | FlAIRS | Invited Talk Abstracts. | Ayanna M. Howard, David Johnson, Cristina Conati, Frederick W. Chen, Nikolaj S. Bjrner |
| 2013 | LPAR | Resourceful Reachability as HORN-LA. | Josh Berdine, Nikolaj S. Bjrner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger |
| 2013 | LPAR | Instantiations, Zippers and EPR Interpolation. | Nikolaj S. Bjrner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav |
| 2013 | LPAR | Effectively Monadic Predicates. | Margus Veanes, Nikolaj S. Bjrner, Lev Nachmanson, Sergey Bereg |
| 2013 | SAS | On Solving Universally Quantified Horn Clauses. | Nikolaj S. Bjrner, Kenneth L. McMillan, Andrey Rybalchenko |
| 2012 | CADE | Taking Satisfiability to the Next Level with Z3 - (Abstract). | Nikolaj S. Bjrner |
| 2012 | CADE | SMT-LIB Sequences and Regular Expressions. | Nikolaj S. Bjrner, Vijay Ganesh, Raphal Michel, Margus Veanes |
| 2012 | CADE | Program Verification as Satisfiability Modulo Theories. | Nikolaj S. Bjrner, Kenneth L. McMillan, Andrey Rybalchenko |
| 2012 | CADE | Anatomy of Alternating Quantifier Satisfiability (Work in progress). | Anh-Dung Phan, Nikolaj S. Bjrner, David Monniaux |
| 2012 | DSN | Latent fault detection in large scale services. | Moshe Gabel, Assaf Schuster, Ran Gilad-Bachrach, Nikolaj S. Bjrner |
| 2012 | LPAR | Engineering Theories with Z3. | Nikolaj S. Bjrner |
| 2012 | MODELS | Detecting Specification Errors in Declarative Languages with Constraints. | Ethan K. Jackson, Wolfram Schulte, Nikolaj S. Bjrner |
| 2012 | POPL | Symbolic finite state transducers: algorithms and applications. | Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj S. Bjrner |
| 2012 | SAT | Generalized Property Directed Reachability. | Krystof Hoder, Nikolaj S. Bjrner |
| 2012 | TACAS | Symbolic Automata: The Toolkit. | Margus Veanes, Nikolaj S. Bjrner |
| 2011 | APLAS | Engineering Theories with Z3. | Nikolaj S. Bjrner |
| 2011 | CAV | Untitled record | Krystof Hoder, Nikolaj S. Bjrner, Leonardo Mendona de Moura |
| 2011 | CPP | Engineering Theories with Z3. | Nikolaj S. Bjrner |
| 2011 | ICLP | Canonical Regular Types. | Ethan K. Jackson, Nikolaj S. Bjrner, Wolfram Schulte |
| 2010 | CADE | Linear Quantifier Elimination as an Abstract Decision Procedure. | Nikolaj S. Bjrner |
| 2010 | CADE | Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2010 | CADE | Applications and Challenges in Satisfiability Modulo Theories. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2010 | LPAR | Symbolic Automata Constraint Solving. | Margus Veanes, Nikolaj S. Bjrner, Leonardo Mendona de Moura |
| 2009 | CAV | Linear Functional Fixed-points. | Nikolaj S. Bjrner, Joe Hendrix |
| 2009 | FMCAD | Generalized, efficient array decision procedures. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2009 | ICTAC | Input-Output Model Programs. | Margus Veanes, Nikolaj S. Bjrner |
| 2009 | SYNASC | SMT Solvers for Testing, Program Analysis and Verification at Microsoft. | Nikolaj S. Bjrner |
| 2009 | TACAS | Path Feasibility Analysis for String-Manipulating Programs. | Nikolaj S. Bjrner, Nikolai Tillmann, Andrei Voronkov |
| 2008 | CADE | Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2008 | CADE | Engineering DPLL(T) + Saturation. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2008 | FORTE | An SMT Approach to Bounded Reachability Analysis of Model Programs. | Margus Veanes, Nikolaj S. Bjrner, Alexander Raschke |
| 2008 | LPAR | Proofs and Refutations, and Z3. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2008 | TACAS | Z3: An Efficient SMT Solver. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2007 | CADE | Efficient E-Matching for SMT Solvers. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 1998 | TACAS | Deciding Fixed and Non-fixed Size Bit-vectors. | Nikolaj S. Bjrner, Mark C. Pichora |
| 1997 | CADE | A Practical Integration of First-Order Reasoning and Decision Procedures. | Nikolaj S. Bjrner, Mark E. Stickel, Toms E. Uribe |
| 1996 | CAV | STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. | Nikolaj S. Bjrner, Anca Browne, Edward Y. Chang, Michael Coln, Arjun Kapur, Zohar Manna, Henny Sipma, Toms E. Uribe |
| 1995 | CP | Automatic Generation of Invariants and Assertions. | Nikolaj S. Bjrner, Anca Browne, Zohar Manna |