Nikolaj S. Bjørner

166 papers A* 16A 24B 17C 3Misc 12Journal 41Unranked 45

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	On Solving String Equations via Powers and Parikh Images. CoRR Clemens Eisenhofer, Theodor Seiser, Nikolaj S. Bjørner, Laura Kovács
2025	J	`jnl`	Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231). Dagstuhl Reports Nikolaj S. Bjørner, Marijn J. H. Heule, Daniela Kaufmann, Jakob Nordström, Wietze Koops
2025	J	`jnl`	LLM-Based Config Synthesis requires Disambiguation. CoRR Rajdeep Mondal, Nikolaj S. Bjørner, Todd D. Millstein, Alan Tang, George Varghese
2025	B	`conf`	On Solving String Equations via Powers and Parikh Images. TABLEAUX Clemens Eisenhofer, Theodor Seiser, Nikolaj S. Bjørner, Laura Kovács
2025	Misc	`conf`	Tackling Ambiguity in User Intent for LLM-based Network Configuration Synthesis. HotNets Rajdeep Mondal, Nikolaj S. Bjørner, Todd D. Millstein, Alan Tang, George Varghese
2025	J	`jnl`	Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling. CoRR Ruanqianqian (Lisa) Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj S. Bjørner
2024	—	`conf`	Arithmetic Solving in Z3. CAV (1) Nikolaj S. Bjørner, Lev Nachmanson
2024	Misc	`conf`	CHISEL: An optical slice of the wide-area network. NSDI Abhishek Vijaya Kumar, Bill Owens, Nikolaj S. Bjørner, Binbin Guan, Yawei Yin, Paramvir Bahl, Rachee Singh
2024	—	`ed.`	LPAR 2024 Complementary Volume, Port Louis, Mauritius, May 26-31, 2024 LPAR Complementary Volume Nikolaj S. Bjørner, Marijn Heule, Andrei Voronkov
2024	B	`ed.`	LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024 LPAR Nikolaj S. Bjørner, Marijn Heule, Andrei Voronkov
2024	—	`conf`	PolySAT: Word-level Bit-vector Reasoning in Z3. VSTTE Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj S. Bjørner, Laura Kovács
2024	J	`jnl`	PolySAT: Word-level Bit-vector Reasoning in Z3. CoRR Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj S. Bjørner, Laura Kovács
2024	J	`jnl`	SpEQ: Translation of Sparse Codes using Equivalences. Proc. ACM Program. Lang. Avery Laird, Bangtian Liu, Nikolaj S. Bjørner, Maryam Mehri Dehnavi
2024	J	`jnl`	Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions. CoRR Nikolaj S. Bjørner, Ashley J. Chen, Shuo Chen, Yang Chen, Zhongxin Guo, Tzu-Han Hsu, Peng Liu, Nanqing Luo
2023	J	`jnl`	An Ethereum-compatible blockchain that explicates and ensures design-level safety properties for smart contracts. CoRR Nikolaj S. Bjørner, Shuo Chen, Yang Chen, Zhongxin Guo, Peng Liu, Nanqing Luo
2023	A	`conf`	On Incremental Pre-processing for SMT. CADE Nikolaj S. Bjørner, Katalin Fazekas
2023	Misc	`conf`	OneWAN is better than two: Unifying a split WAN architecture. NSDI 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
2023	B	`conf`	Satisfiability Modulo Custom Theories in Z3. VMCAI Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács
2023	A*	`conf`	Scalable Optimal Layout Synthesis for NISQ Quantum Processors. DAC Wan-Hsuan Lin, Jason Kimko, Bochen Tan, Nikolaj S. Bjørner, Jason Cong
2022	J	`jnl`	Algebra-Based Reasoning for Loop Synthesis. CoRR Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács
2022	J	`jnl`	Algebra-Based Reasoning for Loop Synthesis. Formal Aspects Comput. Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács
2022	A	`conf`	Analysis of Core-Guided MaxSat Using Cores and Correction Sets. SAT Nina Narodytska, Nikolaj S. Bjørner
2022	Misc	`conf`	Decentralized cloud wide-area network traffic engineering with BLASTSHIELD. NSDI Umesh Krishnaswamy, Rachee Singh, Nikolaj S. Bjørner, Himanshu Raj
2022	—	`conf`	Traffic engineering: from ISP to cloud wide area networks. SOSR Rachee Singh, Nikolaj S. Bjørner, Umesh Krishnaswamy
2022	—	`conf`	User-Propagators for Custom Theories in SMT Solving. SMT Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács
2021	A*	`conf`	Cost-effective capacity provisioning in wide area networks with Shoofly. SIGCOMM Rachee Singh, Nikolaj S. Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette
2021	J	`jnl`	Preface of the special issue on the conference on formal methods in computer aided design 2018. Formal Methods Syst. Des. Nikolaj S. Bjørner, Arie Gurfinkel
2021	J	`jnl`	Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). Dagstuhl Reports Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, Grigore Rosu
2021	B	`conf`	Supercharging Plant Configurations Using Z3. CPAIOR Nikolaj S. Bjørner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati
2021	A*	`conf`	Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. PLDI Caleb Stanford, Margus Veanes, Nikolaj S. Bjørner
2020	B	`conf`	Algebra-Based Loop Synthesis. IFM Andreas Humenberger, Nikolaj S. Bjørner, Laura Kovács
2020	—	`conf`	Navigating the Universe of Z3 Theory Solvers. SBMF Nikolaj S. Bjørner, Lev Nachmanson
2020	B	`conf`	Solving $\mathrm {LIA} ^\star $ Using Approximations. VMCAI Maxwell Levatich, Nikolaj S. Bjørner, Ruzica Piskac, Sharon Shoham
2019	J	`jnl`	Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062). Dagstuhl Reports Sébastien Bardin, Nikolaj S. Bjørner, Cristian Cadar
2019	A	`conf`	Guiding High-Performance SAT Solvers with Unsat-Core Predictions. SAT Daniel Selsam, Nikolaj S. Bjørner
2019	J	`jnl`	NeuroCore: Guiding High-Performance SAT Solvers with Unsat-Core Predictions. CoRR Daniel Selsam, Nikolaj S. Bjørner
2019	—	`ed.`	Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Novosibirsk, Russia, July 2-5, 2019, Revised Selected Papers Ershov Informatics Conference Nikolaj S. Bjørner, Irina B. Virbitskaite, Andrei Voronkov
2019	A	`conf`	Reversible Pebbling Game for Quantum Memory Management. DATE Giulia Meuli, Mathias Soeken, Martin Roetteler, Nikolaj S. Bjørner, Giovanni De Micheli
2019	J	`jnl`	Reversible Pebbling Game for Quantum Memory Management. CoRR Giulia Meuli, Mathias Soeken, Martin Roetteler, Nikolaj S. Bjørner, Giovanni De Micheli
2019	A*	`conf`	TEAVAR: striking the right utilization-availability balance in WAN traffic engineering. SIGCOMM Jeremy Bogle, Nikhil Bhatia, Manya Ghobadi, Ishai Menache, Nikolaj S. Bjørner, Asaf Valadarsky, Michael Schapira
2019	Misc	`conf`	The Science, Art, and Magic of Constrained Horn Clauses. SYNASC Arie Gurfinkel, Nikolaj S. Bjørner
2019	A*	`conf`	Validating datacenters at scale. SIGCOMM 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
2018	B	`ed.`	2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018 FMCAD Nikolaj S. Bjørner, Arie Gurfinkel
2018	A	`conf`	Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. SAT Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv
2018	J	`jnl`	Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. CoRR Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv
2018	A*	`conf`	Core-Guided Minimal Correction Set and Core Enumeration. IJCAI Nina Narodytska, Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv
2018	J	`jnl`	Editorial. Formal Aspects Comput. Nikolaj S. Bjørner, Frank S. de Boer, Andrew Butterfield
2018	J	`jnl`	Preface for the special issue "FM15". Acta Informatica Frank S. de Boer, Nikolaj S. Bjørner
2018	—	`conf`	Programming Z3. SETSS Nikolaj S. Bjørner, Leonardo de Moura, Lev Nachmanson, Christoph M. Wintersteiger
2018	B	`conf`	Z3 and SMT in Industrial R&D. FM Nikolaj S. Bjørner
2017	—	`conf`	Abduction by Non-Experts. LPAR (Short Presentations) Nikolaj S. Bjørner, Dejan Jovanovic, Tancrède Lepoint, Philipp Rümmer, Martin Schäf
2017	—	`conf`	Abduction for Learning Smart City Rules. GCAI Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv
2017	Misc	`conf`	Correct by Construction Networks Using Stepwise Refinement. NSDI Leonid Ryzhyk, Nikolaj S. Bjørner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, George Varghese
2017	J	`jnl`	Monadic Decomposition. J. ACM Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg
2017	A*	`conf`	Optimizing test placement for module-level regression testing. ICSE August Shi, Suresh Thummalapenta, Shuvendu K. Lahiri, Nikolaj S. Bjørner, Jacek Czerwonka
2017	J	`jnl`	Property-Directed Inference of Universal Invariants or Proving Their Absence. J. ACM Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2017	J	`jnl`	Report on Networking and Programming Languages 2017. Comput. Commun. Rev. Nikolaj S. Bjørner, Marco Canini, Nik Sultana
2016	—	`conf`	AVATAR Modulo Theories. GCAI Giles Reger, Nikolaj S. Bjørner, Martin Suda, Andrei Voronkov
2016	A*	`conf`	Cardinalities and universal quantifiers for verifying parameterized systems. PLDI Klaus von Gleissenthall, Nikolaj S. Bjørner, Andrey Rybalchenko
2016	Misc	`ed.`	Distributed Computing and Internet Technology - 12th International Conference, ICDCIT 2016, Bhubaneswar, India, January 15-18, 2016, Proceedings ICDCIT Nikolaj S. Bjørner, Sanjiva Prasad, Laxmi Parida
2016	—	`ch.`	SMT Solvers: Foundations and Applications. Dependable Software Systems Engineering Nikolaj S. Bjørner
2016	A*	`conf`	Scaling network verification using symmetry and surgery. POPL Gordon D. Plotkin, Nikolaj S. Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese
2016	—	`conf`	ddNF: An Efficient Data Structure for Header Spaces. Haifa Verification Conference Nikolaj S. Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese
2015	Misc	`conf`	Checking Beliefs in Dynamic Networks. NSDI Nuno P. Lopes, Nikolaj S. Bjørner, Patrice Godefroid, Karthick Jayaraman, George Varghese
2015	Misc	`conf`	Checking Cloud Contracts in Microsoft Azure. ICDCIT Nikolaj S. Bjørner, Karthick Jayaraman
2015	B	`conf`	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan
2015	J	`jnl`	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan
2015	—	`conf`	Equivalence of Finite-Valued Symbolic Finite Transducers. Ershov Memorial Conference Margus Veanes, Nikolaj S. Bjørner
2015	B	`ed.`	FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings FM Nikolaj S. Bjørner, Frank S. de Boer
2015	J	`jnl`	Formal Foundations for Networking (Dagstuhl Seminar 15071). Dagstuhl Reports Nikolaj S. Bjørner, Nate Foster, Philip Brighten Godfrey, Pamela Zave
2015	—	`conf`	Horn Clause Solvers for Program Verification. Fields of Logic and Computation II Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko
2015	J	`jnl`	Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). Dagstuhl Reports Nikolaj S. Bjørner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, Christoph Weidenbach
2015	A*	`conf`	Maximum Satisfiability Using Cores and Correction Sets. IJCAI Nikolaj S. Bjørner, Nina Narodytska
2015	—	`conf`	On Conflicts and Strategies in QBF. LPAR (short papers) Nikolaj S. Bjørner, Mikolás Janota, William Klieber
2015	—	`conf`	Playing with Quantified Satisfaction. LPAR (short papers) Nikolaj S. Bjørner, Mikolás Janota
2015	B	`conf`	Property Directed Polyhedral Abstraction. VMCAI Nikolaj S. Bjørner, Arie Gurfinkel
2015	—	`conf`	Property-Directed Inference of Universal Invariants or Proving Their Absence. CAV (1) Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2015	J	`jnl`	Symbolic tree automata. Inf. Process. Lett. Margus Veanes, Nikolaj S. Bjørner
2015	A	`conf`	νZ - An Optimizing SMT Solver. TACAS Nikolaj S. Bjørner, Anh-Dung Phan, Lars Fleckenstein
2014	A	`conf`	Computing All Implied Equalities via SMT-Based Partition Refinement. IJCAR Josh Berdine, Nikolaj S. Bjørner
2014	A*	`conf`	Monadic Decomposition. CAV Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg
2014	—	`ed.`	Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014. HCVS Nikolaj S. Bjørner, Fabio Fioravanti, Andrey Rybalchenko, Valerio Senni
2014	A*	`conf`	Property-Directed Shape Analysis. CAV Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur
2014	—	`conf`	Software engineering and automated deduction. FOSE Willem Visser, Nikolaj S. Bjørner, Natarajan Shankar
2014	—	`ch.`	Tractability and Modern Satisfiability Modulo Theories Solvers. Tractability Nikolaj S. Bjørner, Leonardo Mendonça de Moura
2014	A*	`conf`	VeriCon: towards verifying controller programs in software-defined networks. PLDI Thomas Ball, Nikolaj S. Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky
2014	—	`conf`	νZ - Maximal Satisfaction with Z3. SCSS Nikolaj S. Bjørner, Anh-Dung Phan
2013	Misc	`ed.`	15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, September 23-26, 2013 SYNASC Nikolaj S. Bjørner, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen M. Watt, Daniela Zaharie
2013	J	`jnl`	Deduction and Arithmetic (Dagstuhl Seminar 13411). Dagstuhl Reports Nikolaj S. Bjørner, Reiner Hähnle, Tobias Nipkow, Christoph Weidenbach
2013	—	`conf`	Effectively Monadic Predicates. LPAR (short papers) Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg
2013	J	`jnl`	Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
2013	—	`conf`	Instantiations, Zippers and EPR Interpolation. LPAR (short papers) Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav
2013	Misc	`conf`	Invited Talk Abstracts. FLAIRS Ayanna M. Howard, David Johnson, Cristina Conati, Frederick W. Chen, Nikolaj S. Bjørner
2013	B	`conf`	On Solving Universally Quantified Horn Clauses. SAS Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
2013	J	`jnl`	Preface: Special Issue of Selected Extended Papers of CADE-23. J. Autom. Reason. Nikolaj S. Bjørner, Viorica Sofronie-Stokkermans
2013	B	`conf`	Resourceful Reachability as HORN-LA. LPAR Josh Berdine, Nikolaj S. Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger
2013	—	`conf`	Satisfiability modulo theories for high integrity development. HILT Nikolaj S. Bjørner
2012	J	`jnl`	Alternating simulation and IOCO. Int. J. Softw. Tools Technol. Transf. Margus Veanes, Nikolaj S. Bjørner
2012	—	`conf`	Anatomy of Alternating Quantifier Satisfiability (Work in progress). SMT@IJCAR Anh-Dung Phan, Nikolaj S. Bjørner, David Monniaux
2012	—	`conf`	Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN Thomas Ball, Nikolaj S. Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes
2012	A	`conf`	Detecting Specification Errors in Declarative Languages with Constraints. MoDELS Ethan K. Jackson, Wolfram Schulte, Nikolaj S. Bjørner
2012	—	`conf`	Engineering Theories with Z3. IWIL@LPAR Nikolaj S. Bjørner
2012	J	`jnl`	Foreword. J. Symb. Comput. Nikolaj S. Bjørner, Laura Kovács
2012	—	`conf`	From Primal Infon Logic with Individual Variables to Datalog. Correct Reasoning Nikolaj S. Bjørner, Guido de Caso, Yuri Gurevich
2012	J	`jnl`	Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). Dagstuhl Reports Nikolaj S. Bjørner, Krishnendu Chatterjee, Laura Kovács, Rupak Majumdar
2012	A	`conf`	Generalized Property Directed Reachability. SAT Krystof Hoder, Nikolaj S. Bjørner
2012	A	`conf`	Latent fault detection in large scale services. DSN Moshe Gabel, Assaf Schuster, Ran Gilad-Bachrach, Nikolaj S. Bjørner
2012	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings LPAR Nikolaj S. Bjørner, Andrei Voronkov
2012	—	`conf`	Program Verification as Satisfiability Modulo Theories. SMT@IJCAR Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
2012	—	`conf`	SMT in Verification, Modeling, and Testing at Microsoft. Haifa Verification Conference Nikolaj S. Bjørner
2012	—	`conf`	SMT-LIB Sequences and Regular Expressions. SMT@IJCAR Nikolaj S. Bjørner, Vijay Ganesh, Raphaël Michel, Margus Veanes
2012	—	`ed.`	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 WING@ETAPS/IJCAR Andrei Voronkov, Laura Kovács, Nikolaj S. Bjørner
2012	A	`conf`	Symbolic Automata: The Toolkit. TACAS Margus Veanes, Nikolaj S. Bjørner
2012	A*	`conf`	Symbolic finite state transducers: algorithms and applications. POPL Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj S. Bjørner
2012	A	`conf`	Taking Satisfiability to the Next Level with Z3 - (Abstract). IJCAR Nikolaj S. Bjørner
2011	A	`ed.`	Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings CADE Nikolaj S. Bjørner, Viorica Sofronie-Stokkermans
2011	—	`conf`	Canonical Regular Types. ICLP (Technical Communications) Ethan K. Jackson, Nikolaj S. Bjørner, Wolfram Schulte
2011	J	`jnl`	Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2011	B	`conf`	Engineering Theories with Z3. APLAS Nikolaj S. Bjørner
2011	B	`conf`	Engineering Theories with Z3. CPP Nikolaj S. Bjørner
2011	J	`jnl`	Foundations of Finite Symbolic Tree Transducers. Bull. EATCS Margus Veanes, Nikolaj S. Bjørner
2011	J	`jnl`	Satisfiability modulo theories: introduction and applications. Commun. ACM Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2011	—	`conf`	Symbolic Tree Transducers. Ershov Memorial Conference Margus Veanes, Nikolaj S. Bjørner
2010	—	`conf`	10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	—	`conf`	10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	C	`conf`	Alternating Simulation and IOCO. ICTSS Margus Veanes, Nikolaj S. Bjørner
2010	—	`conf`	Applications and Challenges in Satisfiability Modulo Theories. WING@ETAPS/IJCAR Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2010	A	`conf`	Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. IJCAR Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2010	J	`jnl`	Content-dependent chunking for differential compression, the local maximum approach. J. Comput. Syst. Sci. Nikolaj S. Bjørner, Andreas Blass, Yuri Gurevich
2010	—	`conf`	DKAL and Z3: A Logic Embedding Experiment. Fields of Logic and Computation Sergio Mera, Nikolaj S. Bjørner
2010	J	`jnl`	Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reason. Ruzica Piskac, Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2010	—	`ed.`	Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010 Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	A	`conf`	Linear Quantifier Elimination as an Abstract Decision Procedure. IJCAR Nikolaj S. Bjørner
2010	—	`conf`	Symbolic Automata Constraint Solving. LPAR (Yogyakarta) Margus Veanes, Nikolaj S. Bjørner, Leonardo Mendonça de Moura
2009	B	`conf`	Generalized, efficient array decision procedures. FMCAD Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2009	C	`conf`	Input-Output Model Programs. ICTAC Margus Veanes, Nikolaj S. Bjørner
2009	A*	`conf`	Linear Functional Fixed-points. CAV Nikolaj S. Bjørner, Joe Hendrix
2009	A	`conf`	Path Feasibility Analysis for String-Manipulating Programs. TACAS Nikolaj S. Bjørner, Nikolai Tillmann, Andrei Voronkov
2009	Misc	`conf`	SMT Solvers for Testing, Program Analysis and Verification at Microsoft. SYNASC Nikolaj S. Bjørner
2009	—	`conf`	Satisfiability Modulo Theories: An Appetizer. SBMF Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2009	A	`conf`	Specifying and Composing Non-functional Requirements in Model-Based Development. SC Ethan K. Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj S. Bjørner, Wolfram Schulte
2009	—	`conf`	Symbolic Bounded Conformance Checking of Model Programs. Ershov Memorial Conference Margus Veanes, Nikolaj S. Bjørner
2009	J	`jnl`	Symbolic Bounded Model Checking of Abstract State Machines. Int. J. Softw. Informatics Margus Veanes, Nikolaj S. Bjørner, Yuri Gurevich, Wolfram Schulte
2009	—	`conf`	Tapas: Theory Combinations and Practical Applications. FORMATS Nikolaj S. Bjørner, Leonardo Mendonça de Moura
2008	C	`conf`	An SMT Approach to Bounded Reachability Analysis of Model Programs. FORTE Margus Veanes, Nikolaj S. Bjørner, Alexander Raschke
2008	A	`conf`	Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. IJCAR Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2008	A	`conf`	Engineering DPLL(T) + Saturation. IJCAR Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2008	J	`jnl`	Modular difference logic is hard CoRR Nikolaj S. Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi
2008	—	`conf`	Proofs and Refutations, and Z3. LPAR Workshops Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2008	—	`conf`	Using Dynamic Symbolic Execution to Improve Deductive Verification. SPIN Dries Vanoverberghe, Nikolaj S. Bjørner, Jonathan de Halleux, Wolfram Schulte, Nikolai Tillmann
2008	A	`conf`	Z3: An Efficient SMT Solver. TACAS Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2007	A	`conf`	Efficient E-Matching for SMT Solvers. CADE Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2007	—	`conf`	Model-based Theory Combination. SMT@CAV Leonardo Mendonça de Moura, Nikolaj S. Bjørner
2007	—	`conf`	Models and Software Model Checking of a Distributed File Replication System. Formal Methods and Hybrid Real-Time Systems Nikolaj S. Bjørner
2001	J	`jnl`	Deductive verification of real-time systems using STeP. Theor. Comput. Sci. Nikolaj S. Bjørner, Zohar Manna, Henny Sipma, Tomás E. Uribe
2000	—	`conf`	Absolute Explicit Unification. RTA Nikolaj S. Bjørner, César A. Muñoz
2000	J	`jnl`	Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods Syst. Des. Nikolaj S. Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomás E. Uribe
1998	—	`conf`	An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. Tool Support for System Specification, Development and Verification Zohar Manna, Nikolaj S. Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Mark C. Pichora, Henny B. Sipma, Tomás E. Uribe
1998	A	`conf`	Deciding Fixed and Non-fixed Size Bit-vectors. TACAS Nikolaj S. Bjørner, Mark C. Pichora
1998	—	`—`	Integrating decision procedures for temporal verification. Nikolaj S. Bjørner
1997	A	`conf`	A Practical Integration of First-Order Reasoning and Decision Procedures. CADE Nikolaj S. Bjørner, Mark E. Stickel, Tomás E. Uribe
1997	J	`jnl`	Automatic Generation of Invariants and Intermediate Assertions. Theor. Comput. Sci. Nikolaj S. Bjørner, Anca Browne, Zohar Manna
1997	—	`conf`	Deductive Verification of Real-Time Systems Using STeP. ARTS Nikolaj S. Bjørner, Zohar Manna, Henny Sipma, Tomás E. Uribe
1996	A*	`conf`	STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. CAV Nikolaj S. Bjørner, Anca Browne, Edward Y. Chang, Michael Colón, Arjun Kapur, Zohar Manna, Henny Sipma, Tomás E. Uribe
1995	A	`conf`	Automatic Generation of Invariants and Assertions. CP Nikolaj S. Bjørner, Anca Browne, Zohar Manna
1995	—	`conf`	STeP: The Stanford Temporal Prover. TAPSOFT 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