Automatic Generation of Invariants and Assertions. - Nikolaj S. Bjørner; Anca Browne; Zohar Manna (CP, 1995)

STeP: The Stanford Temporal Prover. - 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 (TAPSOFT, 1995)

STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. - Nikolaj S. Bjørner; Anca Browne; Edward Y. Chang; Michael Colón; Arjun Kapur; Zohar Manna; Henny Sipma; Tomás E. Uribe (CAV, 1996)

A Practical Integration of First-Order Reasoning and Decision Procedures. - Nikolaj S. Bjørner; Mark E. Stickel; Tomás E. Uribe (CADE, 1997)

Automatic Generation of Invariants and Intermediate Assertions. - Nikolaj S. Bjørner; Anca Browne; Zohar Manna (Theor. Comput. Sci., 1997)

Deciding Fixed and Non-fixed Size Bit-vectors. - Nikolaj S. Bjørner; Mark C. Pichora (TACAS, 1998)

An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. - Zohar Manna; Nikolaj S. Bjørner; Anca Browne; Michael Colón; Bernd Finkbeiner; Mark C. Pichora; Henny B. Sipma; Tomás E. Uribe (Tool Support for System Specification, Development and Verification, 1998)

Integrating decision procedures for temporal verification. - Nikolaj S. Bjørner (1998)

Absolute Explicit Unification. - Nikolaj S. Bjørner; César A. Muñoz (RTA, 2000)

Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. - Nikolaj S. Bjørner; Anca Browne; Michael Colón; Bernd Finkbeiner; Zohar Manna; Henny Sipma; Tomás E. Uribe (Formal Methods Syst. Des., 2000)

Deductive verification of real-time systems using STeP. - Nikolaj S. Bjørner; Zohar Manna; Henny Sipma; Tomás E. Uribe (Theor. Comput. Sci., 2001)

Models and Software Model Checking of a Distributed File Replication System. - Nikolaj S. Bjørner (Formal Methods and Hybrid Real-Time Systems, 2007)

Efficient E-Matching for SMT Solvers. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (CADE, 2007)

Model-based Theory Combination. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (SMT@CAV, 2007)

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (IJCAR, 2008)

Engineering DPLL(T) + Saturation. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (IJCAR, 2008)

An SMT Approach to Bounded Reachability Analysis of Model Programs. - Margus Veanes; Nikolaj S. Bjørner; Alexander Raschke (FORTE, 2008)

Proofs and Refutations, and Z3. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (LPAR Workshops, 2008)

Using Dynamic Symbolic Execution to Improve Deductive Verification. - Dries Vanoverberghe; Nikolaj S. Bjørner; Jonathan de Halleux; Wolfram Schulte; Nikolai Tillmann (SPIN, 2008)

Z3: An Efficient SMT Solver. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (TACAS, 2008)

Modular difference logic is hard - Nikolaj S. Bjørner; Andreas Blass; Yuri Gurevich; Madan Musuvathi (CoRR, 2008)

Linear Functional Fixed-points. - Nikolaj S. Bjørner; Joe Hendrix (CAV, 2009)

Symbolic Bounded Conformance Checking of Model Programs. - Margus Veanes; Nikolaj S. Bjørner (Ershov Memorial Conference, 2009)

Generalized, efficient array decision procedures. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (FMCAD, 2009)

Tapas: Theory Combinations and Practical Applications. - Nikolaj S. Bjørner; Leonardo Mendonça de Moura (FORMATS, 2009)

Input-Output Model Programs. - Margus Veanes; Nikolaj S. Bjørner (ICTAC, 2009)

Satisfiability Modulo Theories: An Appetizer. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (SBMF, 2009)

Specifying and Composing Non-functional Requirements in Model-Based Development. - Ethan K. Jackson; Dirk Seifert; Markus Dahlweid; Thomas Santen; Nikolaj S. Bjørner; Wolfram Schulte (SC@TOOLS, 2009)

SMT Solvers for Testing, Program Analysis and Verification at Microsoft. - Nikolaj S. Bjørner (SYNASC, 2009)

Path Feasibility Analysis for String-Manipulating Programs. - Nikolaj S. Bjørner; Nikolai Tillmann; Andrei Voronkov (TACAS, 2009)

Symbolic Bounded Model Checking of Abstract State Machines. - Margus Veanes; Nikolaj S. Bjørner; Yuri Gurevich; Wolfram Schulte (Int. J. Softw. Informatics, 2009)

DKAL and Z3: A Logic Embedding Experiment. - Sergio Mera; Nikolaj S. Bjørner (Fields of Logic and Computation, 2010)

Linear Quantifier Elimination as an Abstract Decision Procedure. - Nikolaj S. Bjørner (IJCAR, 2010)

Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (IJCAR, 2010)

Applications and Challenges in Satisfiability Modulo Theories. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (WING@ETAPS/IJCAR, 2010)

10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Decision Procedures in Software, Hardware and Bioware, 2010)

10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Decision Procedures in Software, Hardware and Bioware, 2010)

Symbolic Automata Constraint Solving. - Margus Veanes; Nikolaj S. Bjørner; Leonardo Mendonça de Moura (LPAR (Yogyakarta), 2010)

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. - Ruzica Piskac; Leonardo Mendonça de Moura; Nikolaj S. Bjørner (J. Autom. Reason., 2010)

Content-dependent chunking for differential compression, the local maximum approach. - Nikolaj S. Bjørner; Andreas Blass; Yuri Gurevich (J. Comput. Syst. Sci., 2010)

Engineering Theories with Z3. - Nikolaj S. Bjørner (APLAS, 2011)

μZ- An Efficient Engine for Fixed Points with Constraints. - Krystof Hoder; Nikolaj S. Bjørner; Leonardo Mendonça de Moura (CAV, 2011)

Symbolic Tree Transducers. - Margus Veanes; Nikolaj S. Bjørner (Ershov Memorial Conference, 2011)

Canonical Regular Types. - Ethan K. Jackson; Nikolaj S. Bjørner; Wolfram Schulte (ICLP (Technical Communications), 2011)

Satisfiability modulo theories: introduction and applications. - Leonardo Mendonça de Moura; Nikolaj S. Bjørner (Commun. ACM, 2011)

Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Dagstuhl Reports, 2011)

Foundations of Finite Symbolic Tree Transducers. - Margus Veanes; Nikolaj S. Bjørner (Bull. EATCS, 2011)

From Primal Infon Logic with Individual Variables to Datalog. - Nikolaj S. Bjørner; Guido de Caso; Yuri Gurevich (Correct Reasoning, 2012)

Taking Satisfiability to the Next Level with Z3 - (Abstract). - Nikolaj S. Bjørner (IJCAR, 2012)

SMT-LIB Sequences and Regular Expressions. - Nikolaj S. Bjørner; Vijay Ganesh 001; Raphaël Michel; Margus Veanes (SMT@IJCAR, 2012)

Program Verification as Satisfiability Modulo Theories. - Nikolaj S. Bjørner; Kenneth L. McMillan; Andrey Rybalchenko (SMT@IJCAR, 2012)

Anatomy of Alternating Quantifier Satisfiability (Work in progress). - Anh-Dung Phan; Nikolaj S. Bjørner; David Monniaux (SMT@IJCAR, 2012)

Latent fault detection in large scale services. - Moshe Gabel; Assaf Schuster; Ran Gilad-Bachrach; Nikolaj S. Bjørner (DSN, 2012)

SMT in Verification, Modeling, and Testing at Microsoft. - Nikolaj S. Bjørner (Haifa Verification Conference, 2012)

Detecting Specification Errors in Declarative Languages with Constraints. - Ethan K. Jackson; Wolfram Schulte; Nikolaj S. Bjørner (MoDELS, 2012)

Symbolic finite state transducers: algorithms and applications. - Margus Veanes; Pieter Hooimeijer; Benjamin Livshits; David Molnar; Nikolaj S. Bjørner (POPL, 2012)

Generalized Property Directed Reachability. - Krystof Hoder; Nikolaj S. Bjørner (SAT, 2012)

Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. - Thomas Ball 001; Nikolaj S. Bjørner; Leonardo Mendonça de Moura; Kenneth L. McMillan; Margus Veanes (SPIN, 2012)

Symbolic Automata: The Toolkit. - Margus Veanes; Nikolaj S. Bjørner (TACAS, 2012)

Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). - Nikolaj S. Bjørner; Krishnendu Chatterjee; Laura Kovács; Rupak Majumdar (Dagstuhl Reports, 2012)

Foreword. - Nikolaj S. Bjørner; Laura Kovács (J. Symb. Comput., 2012)

Alternating simulation and IOCO. - Margus Veanes; Nikolaj S. Bjørner (Int. J. Softw. Tools Technol. Transf., 2012)

Invited Talk Abstracts. - Ayanna M. Howard; David Johnson; Cristina Conati; Frederick W. Chen; Nikolaj S. Bjørner (FLAIRS, 2013)

Resourceful Reachability as HORN-LA. - Josh Berdine; Nikolaj S. Bjørner; Samin Ishtiaq; Jael E. Kriener; Christoph M. Wintersteiger (LPAR, 2013)

Instantiations, Zippers and EPR Interpolation. - Nikolaj S. Bjørner; Arie Gurfinkel; Konstantin Korovin; Ori Lahav 001 (LPAR (short papers), 2013)

Effectively Monadic Predicates. - Margus Veanes; Nikolaj S. Bjørner; Lev Nachmanson; Sergey Bereg (LPAR (short papers), 2013)

On Solving Universally Quantified Horn Clauses. - Nikolaj S. Bjørner; Kenneth L. McMillan; Andrey Rybalchenko (SAS, 2013)

Satisfiability modulo theories for high integrity development. - Nikolaj S. Bjørner (HILT, 2013)

Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. - Nikolaj S. Bjørner; Kenneth L. McMillan; Andrey Rybalchenko (CoRR, 2013)

Deduction and Arithmetic (Dagstuhl Seminar 13411). - Nikolaj S. Bjørner; Reiner Hähnle; Tobias Nipkow; Christoph Weidenbach (Dagstuhl Reports, 2013)

Preface: Special Issue of Selected Extended Papers of CADE-23. - Nikolaj S. Bjørner; Viorica Sofronie-Stokkermans (J. Autom. Reason., 2013)

Tractability and Modern Satisfiability Modulo Theories Solvers. - Nikolaj S. Bjørner; Leonardo Mendonça de Moura (Tractability, 2014)

Computing All Implied Equalities via SMT-Based Partition Refinement. - Josh Berdine; Nikolaj S. Bjørner (IJCAR, 2014)

Property-Directed Shape Analysis. - Shachar Itzhaky; Nikolaj S. Bjørner; Thomas W. Reps; Mooly Sagiv; Aditya V. Thakur (CAV, 2014)

Software engineering and automated deduction. - Willem Visser; Nikolaj S. Bjørner; Natarajan Shankar (FOSE, 2014)

VeriCon: towards verifying controller programs in software-defined networks. - Thomas Ball 001; Nikolaj S. Bjørner; Aaron Gember; Shachar Itzhaky; Aleksandr Karbyshev; Mooly Sagiv; Michael Schapira; Asaf Valadarsky (PLDI, 2014)

νZ - Maximal Satisfaction with Z3. - Nikolaj S. Bjørner; Anh-Dung Phan (SCSS, 2014)

Horn Clause Solvers for Program Verification. - Nikolaj S. Bjørner; Arie Gurfinkel; Kenneth L. McMillan; Andrey Rybalchenko (Fields of Logic and Computation II, 2015)

Equivalence of Finite-Valued Symbolic Finite Transducers. - Margus Veanes; Nikolaj S. Bjørner (Ershov Memorial Conference, 2015)

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. - Anvesh Komuravelli; Nikolaj S. Bjørner; Arie Gurfinkel; Kenneth L. McMillan (FMCAD, 2015)

Checking Cloud Contracts in Microsoft Azure. - Nikolaj S. Bjørner; Karthick Jayaraman (ICDCIT, 2015)

Maximum Satisfiability Using Cores and Correction Sets. - Nikolaj S. Bjørner; Nina Narodytska (IJCAI, 2015)

Playing with Quantified Satisfaction. - Nikolaj S. Bjørner; Mikolás Janota (LPAR (short papers), 2015)

On Conflicts and Strategies in QBF. - Nikolaj S. Bjørner; Mikolás Janota; William Klieber (LPAR (short papers), 2015)

Checking Beliefs in Dynamic Networks. - Nuno P. Lopes; Nikolaj S. Bjørner; Patrice Godefroid; Karthick Jayaraman; George Varghese (NSDI, 2015)

νZ - An Optimizing SMT Solver. - Nikolaj S. Bjørner; Anh-Dung Phan; Lars Fleckenstein (TACAS, 2015)

Property Directed Polyhedral Abstraction. - Nikolaj S. Bjørner; Arie Gurfinkel (VMCAI, 2015)

Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). - Nikolaj S. Bjørner; Jasmin Christian Blanchette; Viorica Sofronie-Stokkermans; Christoph Weidenbach (Dagstuhl Reports, 2015)

Formal Foundations for Networking (Dagstuhl Seminar 15071). - Nikolaj S. Bjørner; Nate Foster; Philip Brighten Godfrey; Pamela Zave (Dagstuhl Reports, 2015)

Symbolic tree automata. - Margus Veanes; Nikolaj S. Bjørner (Inf. Process. Lett., 2015)

AVATAR Modulo Theories. - Giles Reger; Nikolaj S. Bjørner; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

ddNF: An Efficient Data Structure for Header Spaces. - Nikolaj S. Bjørner; Garvit Juniwal; Ratul Mahajan; Sanjit A. Seshia; George Varghese (Haifa Verification Conference, 2016)

Cardinalities and universal quantifiers for verifying parameterized systems. - Klaus von Gleissenthall; Nikolaj S. Bjørner; Andrey Rybalchenko (PLDI, 2016)

Scaling network verification using symmetry and surgery. - Gordon D. Plotkin; Nikolaj S. Bjørner; Nuno P. Lopes; Andrey Rybalchenko; George Varghese (POPL, 2016)

SMT Solvers: Foundations and Applications. - Nikolaj S. Bjørner (Dependable Software Systems Engineering, 2016)

Abduction for Learning Smart City Rules. - Nikolaj S. Bjørner; Maria-Cristina V. Marinescu; Mooly Sagiv (GCAI, 2017)

Optimizing test placement for module-level regression testing. - August Shi; Suresh Thummalapenta; Shuvendu K. Lahiri; Nikolaj S. Bjørner; Jacek Czerwonka (ICSE, 2017)

Abduction by Non-Experts. - Nikolaj S. Bjørner; Dejan Jovanovic; Tancrède Lepoint; Philipp Rümmer; Martin Schäf (LPAR (Short Presentations), 2017)

Correct by Construction Networks Using Stepwise Refinement. - Leonid Ryzhyk; Nikolaj S. Bjørner; Marco Canini; Jean-Baptiste Jeannin; Cole Schlesinger; Douglas B. Terry; George Varghese (NSDI, 2017)

Report on Networking and Programming Languages 2017. - Nikolaj S. Bjørner; Marco Canini; Nik Sultana (Comput. Commun. Rev., 2017)

Property-Directed Inference of Universal Invariants or Proving Their Absence. - Aleksandr Karbyshev; Nikolaj S. Bjørner; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (J. ACM, 2017)

Monadic Decomposition. - Margus Veanes; Nikolaj S. Bjørner; Lev Nachmanson; Sergey Bereg (J. ACM, 2017)

Z3 and SMT in Industrial R&D. - Nikolaj S. Bjørner (FM, 2018)

Core-Guided Minimal Correction Set and Core Enumeration. - Nina Narodytska; Nikolaj S. Bjørner; Maria-Cristina V. Marinescu; Mooly Sagiv (IJCAI, 2018)

Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. - Svyatoslav Korneev; Nina Narodytska; Luca Pulina; Armando Tacchella; Nikolaj S. Bjørner; Mooly Sagiv (SAT, 2018)

Programming Z3. - Nikolaj S. Bjørner; Leonardo de Moura 001; Lev Nachmanson; Christoph M. Wintersteiger (SETSS, 2018)

Preface for the special issue "FM15". - Frank S. de Boer; Nikolaj S. Bjørner (Acta Informatica, 2018)

Editorial. - Nikolaj S. Bjørner; Frank S. de Boer; Andrew Butterfield (Formal Aspects Comput., 2018)

Reversible Pebbling Game for Quantum Memory Management. - Giulia Meuli; Mathias Soeken; Martin Roetteler; Nikolaj S. Bjørner; Giovanni De Micheli (DATE, 2019)

Guiding High-Performance SAT Solvers with Unsat-Core Predictions. - Daniel Selsam; Nikolaj S. Bjørner (SAT, 2019)

TEAVAR: striking the right utilization-availability balance in WAN traffic engineering. - Jeremy Bogle; Nikhil Bhatia; Manya Ghobadi; Ishai Menache; Nikolaj S. Bjørner; Asaf Valadarsky; Michael Schapira (SIGCOMM, 2019)

Validating datacenters at scale. - 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; et al. (SIGCOMM, 2019)

The Science, Art, and Magic of Constrained Horn Clauses. - Arie Gurfinkel; Nikolaj S. Bjørner (SYNASC, 2019)

NeuroCore: Guiding High-Performance SAT Solvers with Unsat-Core Predictions. - Daniel Selsam; Nikolaj S. Bjørner (CoRR, 2019)

Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062). - Sébastien Bardin; Nikolaj S. Bjørner; Cristian Cadar (Dagstuhl Reports, 2019)

Algebra-Based Loop Synthesis. - Andreas Humenberger; Nikolaj S. Bjørner; Laura Kovács (IFM, 2020)

Navigating the Universe of Z3 Theory Solvers. - Nikolaj S. Bjørner; Lev Nachmanson (SBMF, 2020)

Solving $ mathrm {LIA} ^ star $ Using Approximations. - Maxwell Levatich; Nikolaj S. Bjørner; Ruzica Piskac; Sharon Shoham (VMCAI, 2020)

Supercharging Plant Configurations Using Z3. - Nikolaj S. Bjørner; Maxwell Levatich; Nuno P. Lopes; Andrey Rybalchenko; Chandrasekar Vuppalapati (CPAIOR, 2021)

Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. - Caleb Stanford; Margus Veanes; Nikolaj S. Bjørner (PLDI, 2021)

Cost-effective capacity provisioning in wide area networks with Shoofly. - Rachee Singh; Nikolaj S. Bjørner; Sharon Shoham; Yawei Yin; John Arnold; Jamie Gaudette (SIGCOMM, 2021)

Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). - Nikolaj S. Bjørner; Maria Christakis; Matteo Maffei; Grigore Rosu (Dagstuhl Reports, 2021)

Preface of the special issue on the conference on formal methods in computer aided design 2018. - Nikolaj S. Bjørner; Arie Gurfinkel (Formal Methods Syst. Des., 2021)

Decentralized cloud wide-area network traffic engineering with BLASTSHIELD. - Umesh Krishnaswamy; Rachee Singh; Nikolaj S. Bjørner; Himanshu Raj (NSDI, 2022)

Analysis of Core-Guided MaxSat Using Cores and Correction Sets. - Nina Narodytska; Nikolaj S. Bjørner (SAT, 2022)

User-Propagators for Custom Theories in SMT Solving. - Nikolaj S. Bjørner; Clemens Eisenhofer; Laura Kovács (SMT, 2022)

Traffic engineering: from ISP to cloud wide area networks. - Rachee Singh; Nikolaj S. Bjørner; Umesh Krishnaswamy (SOSR, 2022)

Algebra-Based Reasoning for Loop Synthesis. - Andreas Humenberger; Daneshvar Amrollahi; Nikolaj S. Bjørner; Laura Kovács (Formal Aspects Comput., 2022)

On Incremental Pre-processing for SMT. - Nikolaj S. Bjørner; Katalin Fazekas (CADE, 2023)

Scalable Optimal Layout Synthesis for NISQ Quantum Processors. - Wan-Hsuan Lin; Jason Kimko; Bochen Tan; Nikolaj S. Bjørner; Jason Cong (DAC, 2023)

OneWAN is better than two: Unifying a split WAN architecture. - 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; et al. (NSDI, 2023)

Satisfiability Modulo Custom Theories in Z3. - Nikolaj S. Bjørner; Clemens Eisenhofer; Laura Kovács (VMCAI, 2023)

An Ethereum-compatible blockchain that explicates and ensures design-level safety properties for smart contracts. - Nikolaj S. Bjørner; Shuo Chen; Yang Chen; Zhongxin Guo; Peng Liu; Nanqing Luo (CoRR, 2023)

Arithmetic Solving in Z3. - Nikolaj S. Bjørner; Lev Nachmanson (CAV (1), 2024)

CHISEL: An optical slice of the wide-area network. - Abhishek Vijaya Kumar; Bill Owens; Nikolaj S. Bjørner; Binbin Guan; Yawei Yin; Paramvir Bahl; Rachee Singh (NSDI, 2024)

PolySAT: Word-level Bit-vector Reasoning in Z3. - Jakob Rath; Clemens Eisenhofer; Daniela Kaufmann; Nikolaj S. Bjørner; Laura Kovács (VSTTE, 2024)

Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions. - Nikolaj S. Bjørner; Ashley J. Chen; Shuo Chen; Yang Chen; Zhongxin Guo; Tzu-Han Hsu; Peng Liu; Nanqing Luo (CoRR, 2024)

SpEQ: Translation of Sparse Codes using Equivalences. - Avery Laird; Bangtian Liu; Nikolaj S. Bjørner; Maryam Mehri Dehnavi (Proc. ACM Program. Lang., 2024)

Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling. - Ruanqianqian (Lisa) Huang; Ayana Monroe; Peli de Halleux; Sorin Lerner; Nikolaj S. Bjørner (CoRR, 2025)

LLM-Based Config Synthesis requires Disambiguation. - Rajdeep Mondal; Nikolaj S. Bjørner; Todd D. Millstein; Alan Tang; George Varghese (CoRR, 2025)