Nikolaj S. Bjørner

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

Decentralized cloud wide-area network traffic engineering with BLASTSHIELD.

[BibT_eX]

[DOI]

Proceedings of the 19th USENIX Symposium on Networked Systems Design and Implementation, 2022

2021

Preface of the special issue on the conference on formal methods in computer aided design 2018.

[BibT_eX]

[DOI]

Arie Gurfinkel

Formal Methods Syst. Des., 2021

Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2021

Cost-effective capacity provisioning in wide area networks with Shoofly.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGCOMM 2021 Conference, Virtual Event, USA, August 23-27, 2021., 2021

Symbolic Boolean derivatives for efficiently solving extended regular expression constraints.

[BibT_eX]

[DOI]

Caleb Stanford

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Supercharging Plant Configurations Using Z3.

[BibT_eX]

[DOI]

Chandrasekar Vuppalapati

Proceedings of the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, 2021

2020

Solving $\mathrm {LIA} ^\star $ Using Approximations.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Navigating the Universe of Z3 Theory Solvers.

[BibT_eX]

[DOI]

Lev Nachmanson

Proceedings of the Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, 2020

Algebra-Based Loop Synthesis.

[BibT_eX]

[DOI]

Andreas Humenberger

Laura Kovács

Proceedings of the Integrated Formal Methods - 16th International Conference, 2020

2019

Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062).

[BibT_eX]

[DOI]

Sébastien Bardin

Cristian Cadar

Dagstuhl Reports, 2019

NeuroCore: Guiding High-Performance SAT Solvers with Unsat-Core Predictions.

[BibT_eX]

[DOI]

Daniel Selsam

CoRR, 2019

The Science, Art, and Magic of Constrained Horn Clauses.

[BibT_eX]

[DOI]

Arie Gurfinkel

Paul-Andre C. Bissonnette

Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2019

Validating datacenters at scale.

[BibT_eX]

[DOI]

Proceedings of the ACM Special Interest Group on Data Communication, 2019

TEAVAR: striking the right utilization-availability balance in WAN traffic engineering.

[BibT_eX]

[DOI]

Proceedings of the ACM Special Interest Group on Data Communication, 2019

Guiding High-Performance SAT Solvers with Unsat-Core Predictions.

[BibT_eX]

[DOI]

Daniel Selsam

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Reversible Pebbling Game for Quantum Memory Management.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2019

2018

Editorial.

[BibT_eX]

[DOI]

Frank S. de Boer

Andrew Butterfield

Formal Aspects Comput., 2018

Preface for the special issue "FM15".

[BibT_eX]

[DOI]

Frank S. de Boer

Acta Informatica, 2018

Programming Z3.

[BibT_eX]

[DOI]

Christoph M. Wintersteiger

Leonardo de Moura

Lev Nachmanson

Proceedings of the Engineering Trustworthy Software Systems - 4th International School, 2018

Constrained Image Generation Using Binarized Neural Networks with Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Core-Guided Minimal Correction Set and Core Enumeration.

[BibT_eX]

[DOI]

Nina Narodytska

Maria-Cristina V. Marinescu

Mooly Sagiv

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

Z3 and SMT in Industrial R&D.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017

Monadic Decomposition.

[BibT_eX]

[DOI]

J. ACM, 2017

Property-Directed Inference of Universal Invariants or Proving Their Absence.

[BibT_eX]

[DOI]

J. ACM, 2017

Report on Networking and Programming Languages 2017.

[BibT_eX]

[DOI]

Marco Canini

Nik Sultana

Comput. Commun. Rev., 2017

Correct by Construction Networks Using Stepwise Refinement.

[BibT_eX]

[DOI]

Leonid Ryzhyk

Marco Canini

Jean-Baptiste Jeannin

Cole Schlesinger

Douglas B. Terry

George Varghese

Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, 2017

Abduction by Non-Experts.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Optimizing test placement for module-level regression testing.

[BibT_eX]

[DOI]

Proceedings of the 39th International Conference on Software Engineering, 2017

Abduction for Learning Smart City Rules.

[BibT_eX]

[DOI]

Maria-Cristina V. Marinescu

Mooly Sagiv

Proceedings of the GCAI 2017, 2017

2016

SMT Solvers: Foundations and Applications.

[BibT_eX]

[DOI]

Proceedings of the Dependable Software Systems Engineering, 2016

Scaling network verification using symmetry and surgery.

[BibT_eX]

[DOI]

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Cardinalities and universal quantifiers for verifying parameterized systems.

[BibT_eX]

[DOI]

Klaus von Gleissenthall

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

ddNF: An Efficient Data Structure for Header Spaces.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2016

AVATAR Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

2015

Symbolic tree automata.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2015

Formal Foundations for Networking (Dagstuhl Seminar 15071).

[BibT_eX]

[DOI]

Nate Foster

Philip Brighten Godfrey

Pamela Zave

Dagstuhl Reports, 2015

Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381).

[BibT_eX]

[DOI]

Jasmin Christian Blanchette

Viorica Sofronie-Stokkermans

Christoph Weidenbach

Dagstuhl Reports, 2015

Property Directed Polyhedral Abstraction.

[BibT_eX]

[DOI]

Arie Gurfinkel

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

νZ - An Optimizing SMT Solver.

[BibT_eX]

[DOI]

Anh-Dung Phan

Lars Fleckenstein

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Checking Beliefs in Dynamic Networks.

[BibT_eX]

[DOI]

Proceedings of the 12th USENIX Symposium on Networked Systems Design and Implementation, 2015

On Conflicts and Strategies in QBF.

[BibT_eX]

[DOI]

Mikolás Janota

William Klieber

Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

Playing with Quantified Satisfaction.

[BibT_eX]

[DOI]

Mikolás Janota

Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

Maximum Satisfiability Using Cores and Correction Sets.

[BibT_eX]

[DOI]

Nina Narodytska

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Checking Cloud Contracts in Microsoft Azure.

[BibT_eX]

[DOI]

Karthick Jayaraman

Proceedings of the Distributed Computing and Internet Technology, 2015

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2015

Equivalence of Finite-Valued Symbolic Finite Transducers.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of System Informatics, 2015

Horn Clause Solvers for Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Fields of Logic and Computation II, 2015

2014

νZ - Maximal Satisfaction with Z3.

[BibT_eX]

[DOI]

Anh-Dung Phan

Proceedings of the 6th International Symposium on Symbolic Computation in Software Science, 2014

VeriCon: towards verifying controller programs in software-defined networks.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Software engineering and automated deduction.

[BibT_eX]

[DOI]

Willem Visser

Natarajan Shankar

Proceedings of the on Future of Software Engineering, 2014

Property-Directed Shape Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Computing All Implied Equalities via SMT-Based Partition Refinement.

[BibT_eX]

[DOI]

Josh Berdine

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

Tractability and Modern Satisfiability Modulo Theories Solvers.

[BibT_eX]

[DOI]

Proceedings of the Tractability: Practical Approaches to Hard Problems, 2014

2013

Preface: Special Issue of Selected Extended Papers of CADE-23.

[BibT_eX]

[DOI]

Viorica Sofronie-Stokkermans

J. Autom. Reason., 2013

Deduction and Arithmetic (Dagstuhl Seminar 13411).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2013

Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types.

[BibT_eX]

[DOI]

CoRR, 2013

Satisfiability modulo theories for high integrity development.

[BibT_eX]

[DOI]

Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, 2013

On Solving Universally Quantified Horn Clauses.

[BibT_eX]

[DOI]

Christoph M. Wintersteiger

Proceedings of the Static Analysis - 20th International Symposium, 2013

Effectively Monadic Predicates.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2013, 2013

Instantiations, Zippers and EPR Interpolation.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2013, 2013

Resourceful Reachability as HORN-LA.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Invited Talk Abstracts.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth International Florida Artificial Intelligence Research Society Conference, 2013

2012

Alternating simulation and IOCO.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2012

Foreword.

[BibT_eX]

[DOI]

Laura Kovács

J. Symb. Comput., 2012

Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461).

[BibT_eX]

[DOI]

Krishnendu Chatterjee

Laura Kovács

Rupak Majumdar

Dagstuhl Reports, 2012

Symbolic Automata: The Toolkit.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials.

[BibT_eX]

[DOI]

Thomas Ball

Proceedings of the Model Checking Software - 19th International Workshop, 2012

Generalized Property Directed Reachability.

[BibT_eX]

[DOI]

Krystof Hoder

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Symbolic finite state transducers: algorithms and applications.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Detecting Specification Errors in Declarative Languages with Constraints.

[BibT_eX]

[DOI]

Ethan K. Jackson

Wolfram Schulte

Proceedings of the Model Driven Engineering Languages and Systems, 2012

Engineering Theories with Z3.

[BibT_eX]

[DOI]

Proceedings of the IWIL 2012: The 9th International Workshop on the Implementation of Logics, 2012

SMT in Verification, Modeling, and Testing at Microsoft.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2012

Latent fault detection in large scale services.

[BibT_eX]

[DOI]

Proceedings of the IEEE/IFIP International Conference on Dependable Systems and Networks, 2012

Anatomy of Alternating Quantifier Satisfiability (Work in progress).

[BibT_eX]

[DOI]

Anh-Dung Phan

David Monniaux

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Program Verification as Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

SMT-LIB Sequences and Regular Expressions.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Taking Satisfiability to the Next Level with Z3 - (Abstract).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

From Primal Infon Logic with Individual Variables to Datalog.

[BibT_eX]

[DOI]

Guido de Caso

Yuri Gurevich

Proceedings of the Correct Reasoning, 2012

2011

Foundations of Finite Symbolic Tree Transducers.

[BibT_eX]

[DOI]

Bull. EATCS, 2011

Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2011

Satisfiability modulo theories: introduction and applications.

[BibT_eX]

[DOI]

Commun. ACM, 2011

Canonical Regular Types.

[BibT_eX]

[DOI]

Ethan K. Jackson

Wolfram Schulte

Proceedings of the Technical Communications of the 27th International Conference on Logic Programming, 2011

Symbolic Tree Transducers.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of Systems Informatics, 2011

<i>μZ</i>- An Efficient Engine for Fixed Points with Constraints.

[BibT_eX]

[DOI]

Krystof Hoder

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

Content-dependent chunking for differential compression, the local maximum approach.

[BibT_eX]

[DOI]

Andreas Blass

Yuri Gurevich

J. Comput. Syst. Sci., 2010

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets.

[BibT_eX]

[DOI]

Ruzica Piskac

J. Autom. Reason., 2010

Symbolic Automata Constraint Solving.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware.

[BibT_eX]

[DOI]

Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware.

[BibT_eX]

[DOI]

Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

Applications and Challenges in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Invariant Generation, 2010

Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Linear Quantifier Elimination as an Abstract Decision Procedure.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

DKAL and Z3: A Logic Embedding Experiment.

[BibT_eX]

[DOI]

Sergio Mera

Proceedings of the Fields of Logic and Computation, 2010

2009

Symbolic Bounded Model Checking of Abstract State Machines.

[BibT_eX]

[DOI]

Int. J. Softw. Informatics, 2009

Path Feasibility Analysis for String-Manipulating Programs.

[BibT_eX]

[DOI]

Nikolai Tillmann

Andrei Voronkov

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

SMT Solvers for Testing, Program Analysis and Verification at Microsoft.

[BibT_eX]

[DOI]

Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

Specifying and Composing Non-functional Requirements in Model-Based Development.

[BibT_eX]

[DOI]

Proceedings of the Software Composition - 8th International Conference, 2009

Satisfiability Modulo Theories: An Appetizer.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods: Foundations and Applications, 2009

Input-Output Model Programs.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2009

Tapas: Theory Combinations and Practical Applications.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2009

Generalized, efficient array decision procedures.

[BibT_eX]

[DOI]

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Symbolic Bounded Conformance Checking of Model Programs.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of Systems Informatics, 2009

Linear Functional Fixed-points.

[BibT_eX]

[DOI]

Joe Hendrix

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Modular difference logic is hard

[BibT_eX]

[DOI]

CoRR, 2008

Z3: An Efficient SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Using Dynamic Symbolic Execution to Improve Deductive Verification.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2008

Proofs and Refutations, and Z3.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2008 Workshops, 2008

An SMT Approach to Bounded Reachability Analysis of Model Programs.

[BibT_eX]

[DOI]

Alexander Raschke

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008

Engineering DPLL(T) + Saturation.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Model-based Theory Combination.

[BibT_eX]

[DOI]

Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, 2007

Efficient E-Matching for SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

Models and Software Model Checking of a Distributed File Replication System.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2001

Deductive verification of real-time systems using STeP.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2001

2000

Verifying Temporal Properties of Reactive Systems: A STeP Tutorial.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2000

Absolute Explicit Unification.

[BibT_eX]

[DOI]

César A. Muñoz

Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

1998

Integrating decision procedures for temporal verification.

[BibT_eX]

[DOI]

PhD thesis, 1998

An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the International Workshop Tool Support for System Specification, 1998

Deciding Fixed and Non-fixed Size Bit-vectors.

[BibT_eX]

[DOI]

Mark C. Pichora

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

1997

Automatic Generation of Invariants and Intermediate Assertions.

[BibT_eX]

[DOI]

Anca Browne

Zohar Manna

Theor. Comput. Sci., 1997

A Practical Integration of First-Order Reasoning and Decision Procedures.

[BibT_eX]

[DOI]

Mark E. Stickel

Tomás E. Uribe

Proceedings of the Automated Deduction, 1997

1996

STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995

STeP: The Stanford Temporal Prover.

[BibT_eX]

[DOI]

Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Automatic Generation of Invariants and Assertions.

[BibT_eX]

[DOI]