Clark Barrett's Publications

Also see publications by date

Contents:

Book Chapters

Satisfiability Modulo Theories (Handbook of Satisfiability, 2009)
Proofs in Satisfiability Modulo Theories (All about Proofs, Proofs for All, 2015)
Satisfiability Modulo Theories (Handbook of Model Checking, 2018)
Satisfiability Modulo Theories (Handbook of Satisfiability, Second Edition, 2021)

Book Reviews

“Decision Procedures:An Algorithmic Point of View,” by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008 (Journal of Automated Reasoning, 2013)

Conference Publications

Automatic Generation of Invariants in Processor Verification (Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96), 1996)
Validity Checking for Combinations of Theories with Equality (Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96), 1996)
A Decision Procedure for Bit-vector Arithmetic (Proceedings of the 35^th Design Automation Conference (DAC '98), 1998)
A Framework for Cooperating Decision Procedures (Proceedings of the 17^th International Conference on Computer-Aided Deduction (CADE '00), 2000)
A Decision Procedure for an Extensional Theory of Arrays (Proceedings of the 16^th IEEE Symposium on Logic in Computer Science (LICS '01), 2001)
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02), 2002)
CVC: A Cooperating Validity Checker (Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02), 2002)
CVC Lite: A New Implementation of the Cooperating Validity Checker (Proceedings of the 16^th International Conference on Computer Aided Verification (CAV '04), 2004)
Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations (Proceedings of the 2^nd IEEE International Conference on Software Engineering and Formal Methods (SEFM '04), 2004)
SMT-COMP: Satisfiability Modulo Theories Competition (Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05), 2005)
TVOC: A Translation Validator for Optimizing Compilers (Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05), 2005)
CASCADE: C Assertion Checker and Deductive Engine (Proceedings of the 18^th International Conference on Computer Aided Verification (CAV '06), 2006)
Splitting on Demand in SAT Modulo Theories (Proceedings of the 13^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '06), 2006)
Solving Quantified Verification Conditions using Satisfiability Modulo Theories (Proceedings of the 21^st International Conference on Automated Deduction (CADE '07), 2007)
CVC3 (Proceedings of the 19^th International Conference on Computer Aided Verification (CAV '07), 2007)
Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors (Proceedings of the 15^th International Static Analysis Symposium (SAS '08), 2008)
Verifying Low-Level Implementations of High-Level Datatypes (Proceedings of the 22^nd International Conference on Computer Aided Verification (CAV '10), 2010)
Polite Theories Revisited (Proceedings of the 17^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10), 2010)
CVC4 (Proceedings of the 23^rd International Conference on Computer Aided Verification (CAV '11), 2011)
Sharing is Caring: Combination of Theories (Proceedings of the 8^th International Symposium on Frontiers of Combining Systems (FroCoS '11), 2011)
Witness Runs for Counter Machines (Proceedings of the 9^th International Symposium on Frontiers of Combining Systems (FroCoS '13), 2013)
Simplex with Sum of Infeasibilities for SMT (Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), 2013)
The Design and Implementation of the Model Constructing Satisfiability Calculus (Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), 2013)
Quantifier Instantiation Techniques for Finite Model Finding in SMT (Proceedings of the 24^th International Conference on Automated Deduction (CADE '13), 2013)
Cascade 2.0 (Proceedings of the 15^th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '14), 2014)
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14), 2014)
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14), 2014)
Leveraging Linear and Mixed Integer Programming for SMT (Proceedings of the 14^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '14), 2014)
Cascade (Competition Contribution) (Proceedings of the 21^st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '15), 2015)
Counterexample Guided Quantifier Instantiation for Synthesis in SMT (Proceedings of the 27^th International Conference on Computer Aided Verification (CAV '15), 2015)
Deciding Local Theory Extensions via E-matching (Proceedings of the 27^th International Conference on Computer Aided Verification (CAV '15), 2015)
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings (Proceedings of the 10^th International Symposium on Frontiers of Combining Systems (FroCoS '15), 2015)
Theory-Aided Model Checking of Concurrent Transition Systems (Proceedings of the 15^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '15), 2015)
A Structured Approach to Post-Silicon Validation and Debug using Symbolic Quick Error Detection (Proceedings of the 42^nd International Test Conference (ITC '15), 2015)
Fine-grained SMT Proofs for the Theory of Fixed-width Bit-vectors (Proceedings of the 20^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '15), 2015)
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (Proceedings of the 8^th International Joint Conference on Automated Reasoning (IJCAR '16), 2016)
Lazy Proofs for DPLL(T)-Based SMT Solvers (Proceedings of the 16^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '16), 2016)
Partitioned Memory Models for Program Analysis (Proceedings of the 18^th International Conference on Verification, Model Checking, and Abstract Interpretion (VMCAI '17), 2017)
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), 2017)
Scaling up DPLL(T) String Solvers Using Context-Dependent Simplification (Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), 2017)
E-QED: Electrical Bug Localization During Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods (Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), 2017)
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), 2017)
Relational Constraint Solving in SMT (Proceedings of the 26^th International Conference on Automated Deduction (CADE '17), 2017)
Designing Theory Solvers with Extensions (Proceedings of the 11^th International Symposium on Frontiers of Combining Systems (FroCoS '17), 2017)
Symbolic quick error detection using symbolic initial state for pre-silicon verification (Proceedings of the 2018 Design, Automation and Test in Europe (DATE '18), 2018)
p4pktgen: Automated Test Case Generation for P4 Programs (Proceedings of the ACM Symposium on SDN Research (SOSR '18), 2018)
EMME: a formal tool for ECMAScript Memory Model Evaluation (Proceedings of the 24^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '18), 2018)
Datatypes with Shared Selectors (Proceedings of the 9^th International Joint Conference on Automated Reasoning (IJCAR '18), 2018)
Solving Quantified Bit-Vectors using Invertibility Conditions (Proceedings of the 30^th International Conference on Computer Aided Verification (CAV '18), 2018)
DeepSafe: A Data-driven Approach for Assessing Robustness of Neural Networks (Proceedings of the 16^th International Symposium on Automated Technology for Verification and Analysis (ATVA '18), 2018)
CoSA: Integrated Verification for Agile Hardware Design (Proceedings of the 18^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '18), 2018)
Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking (Proceedings of the 2019 Design, Automation and Test in Europe (DATE '19), 2019)
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study (Proceedings of the 2019 Design, Automation and Test in Europe (DATE '19), 2019)
High-Level Abstractions for Simplifying Extended String Constraints in SMT (Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), 2019)
Invertibility Conditions for Floating-Point Formulas (Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), 2019)
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers (Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19), 2019)
The Marabou Framework for Verification and Analysis of Deep Neural Networks (Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), 2019)
CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), 2019)
DRAT-based Bit-Vector Proofs in CVC4 (Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19), 2019)
Extending SMT Solvers to Higher-Order Logic (Proceedings of the 27^th International Conference on Automated Deduction (CADE '19), 2019)
Towards Bit-Width-Independent Proofs in SMT Solvers (Proceedings of the 27^th International Conference on Automated Deduction (CADE '19), 2019)
Integration and Flight Test of Small UAS Detect and Avoid on A Miniaturized Avionics Platform (Proceedings of the 38^th Digital Avionics Systems Conference (DASC '19), 2019)
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper (Proceedings of the International Conference on Computer-Aided Design (ICCAD '19), 2019)
Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks (Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig '19), 2019)
G2SAT: Learning to Generate SAT Formulas (Advances in Neural Information Processing Systems 32 (NeurIPS '19), 2019)
Gap-Free Processor Verification by S^2QED and Property Generation (Proceedings of the 2020 Design, Automation and Test in Europe (DATE '20), 2020)
Partial Order Reduction for Deep Bug Finding in Synchronous Hardware (Proceedings of the 26^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '20), 2020)
Simplifying Neural Networks using Formal Verification (NASA Formal Methods: 12th International Symposium, (NFM '20), 2020)
A Decision Procedure for String to Code Point Conversion (Proceedings of the 9^th International Joint Conference on Automated Reasoning (IJCAR '20), 2020)
Creating an Agile Hardware Design Flow (Proceedings of the 57^th Design Automation Conference (DAC '20), 2020)
Politeness for the Theory of Algebraic Datatypes (Proceedings of the 10^th International Joint Conference on Automated Reasoning (IJCAR '20), 2020)
The Move Prover (Proceedings of the 32^nd International Conference on Computer Aided Verification (CAV '20), 2020)
fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components (Proceedings of the 32^nd International Conference on Computer Aided Verification (CAV '20), 2020)
A-QED Verification of Hardware Accelerators (Proceedings of the 57^th Design Automation Conference (DAC '20), 2020)
A Theoretical Framework for Symbolic Quick Error Detection (Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20), 2020)
Parallelization Techniques for Verifying Neural Networks (Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20), 2020)
Reductions for Strings and Regular Expressions Revisited (Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20), 2020)
Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance (Proceedings of the 39^th Digital Avionics Systems Conference (DASC '20), 2020)
Verifying Recurrent Neural Networks Using Invariant Inference (Proceedings of the 18^th International Symposium on Automated Technology for Verification and Analysis (ATVA '20), 2020)
An SMT-Based Approach for Verifying Binarized Neural Networks (Proceedings of the 27^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), 2021)
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (Proceedings of the 27^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), 2021)
Syntax-Guided Quantifier Instantiation (Proceedings of the 27^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), 2021)
Politeness and Stable Infiniteness: Stronger Together (Proceedings of the 28^th International Conference on Automated Deduction (CADE '21), 2021)
Pono: A Flexible and Extensible SMT-based Model Checker (Proceedings of the 33^rd International Conference on Computer Aided Verification (CAV '21), 2021)
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving (Proceedings of the 24^th International Conference on Theory and Applications of Satisfiability Testing (SAT '21), 2021)
DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers (Computer Safety, Reliability, and Security (SAFECOMP '21), 2021)
Automating System Configuration (Proceedings of the 21^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '21), 2021)
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition (Proceedings of the 21^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '21), 2021)
SAT Solving in the Serverless Cloud (Proceedings of the 21^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '21), 2021)
Bit-Precise Reasoning via Int-Blasting (Proceedings of the 23^rd International Conference on Verification, Model Checking, and Abstract Interpretion (VMCAI '22), 2022)
Efficient Neural Network Analysis with Sum-of-Infeasibilities (Proceedings of the 28^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '22), 2022)
cvc5: A Versatile and Industrial-Strength SMT Solver (Proceedings of the 28^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '22), 2022)
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description) (Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), 2022)
Even Faster Conflicts and Lazier Reductions for String Solvers (Proceedings of the 34^th International Conference on Computer Aided Verification (CAV '22), 2022)
Flexible Proof Production in an Industrial-Strength SMT Solver (Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), 2022)
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (Proceedings of the 34^th International Conference on Computer Aided Verification (CAV '22), 2022)
Reasoning About Vectors Using an SMT Theory of Sequences (Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), 2022)
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (Proceedings of the 20^th International Symposium on Automated Technology for Verification and Analysis (ATVA '22), 2022)
Neural Network Verification with Proof Production (Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), 2022)
On Optimizing Back-Substitution Methods for Neural Network Verification (Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), 2022)
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers (Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), 2022)
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language (Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), 2022)
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT (Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), 2022)
Toward Certified Robustness Against Real-World Distribution Shifts (Proceedings of the 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML), 2023)
An Interactive SMT Tactic in Coq using Abductive Reasoning (Proceedings of 24^th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '23), 2023)
Tighter Abstract Queries in Neural Network Verification (Proceedings of 24^th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '23), 2023)
APEX: A Framework for Automated Processing Element Design Space Exploration using Frequent Subgraph Analysis (Proceedings of the 28^th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Volume 3, 2023)
Convex Bounds on the Softmax Function with Applications to Robustness Verification (Proceedings of The 26^th International Conference on Artificial Intelligence and Statistics (AISTATS '23), 2023)
Bounded Verification for Finite-Field-Blasting (Proceedings of the 35^th International Conference on Computer Aided Verification (CAV '23), 2023)
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness (Proceedings of the 29^th International Conference on Automated Deduction (CADE '23), 2023)
Satisfiability Modulo Finite Fields (Proceedings of the 35^th International Conference on Computer Aided Verification (CAV '23), 2023)
G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators (Proceedings of the 60^th Design Automation Conference (DAC '23), 2023)
Combining Finite Combination Properties: Finite Models and Busy Beavers (Proceedings of the 14^th International Symposium on Frontiers of Combining Systems (FroCoS '23), 2023)
Formal Verification of Bit-Vector Invertibility Conditions in Coq (Proceedings of the 14^th International Symposium on Frontiers of Combining Systems (FroCoS '23), 2023)
DNN Verification, Reachability, and the Exponential Function Problem (34^th International Conference on Concurrency Theory (CONCUR '23), 2023)
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery (Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), 2023)
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning (Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), 2023)
Partitioning Strategies for Distributed SMT Solving (Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), 2023)
Soy: An Efficient MILP Solver for Piecewise-Affine Systems (2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS '23), 2023)
H_2O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models (Advances in Neural Information Processing Systems 36 (NeurIPS 2023), 2023)
Towards Optimal Caching and Model Selection for Large Model Inference (Advances in Neural Information Processing Systems 36 (NeurIPS 2023), 2023)
VeriX: Towards Verified Explainability of Deep Neural Networks (Advances in Neural Information Processing Systems 36 (NeurIPS 2023), 2023)
Towards Efficient Verification of Quantized Neural Networks (Proceedings of the AAAI Conference on Artificial Intelligence (AAAI-24), 2024)
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL (Proceedings of the 30^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '24), 2024)
Lemur: Integrating Large Language Models in Automated Program Verification (The Twelfth International Conference on Learning Representations (ICLR '24), 2024)
Verifying SQL queries using theories of tables and relations (Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '24), 2024)
Clover: Closed-Loop Verifiable Code Generation (Proceedings of the First International Symposium on AI Verification (SAIV '24), 2024)
Generalized Optimization Modulo Theories (Proceedings of the 12^th International Joint Conference on Automated Reasoning (IJCAR '24), 2024)
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks (Proceedings of the 36^th International Conference on Computer Aided Verification (CAV '24), 2024)
Parallel Verification for delta-Equivalence of Neural Network Quantization (Proceedings of the First International Symposium on AI Verification (SAIV '24), 2024)
Split Gröbner Bases for Satisfiability Modulo Finite Fields (Proceedings of the 36^th International Conference on Computer Aided Verification (CAV '24), 2024)
Robust Mean Estimation by All Means (Proceedings of the 15^th International Conference on Interactive Theorem Proving (ITP 2024), 2024)
Safe and Reliable Training of Learning-Based Aerospace Controllers (2024 AIAA DATC/IEEE 43^rd Digital Avionics Systems Conference (DASC '24), 2024)
Satisfiability Modulo Theories: A Beginner's Tutorial (Proceedings of the 26^th International Symposium on Formal Methods (FM '24), Part II, 2024)
The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems (Proceedings of the 26^th International Symposium on Formal Methods (FM '24), Part I, 2024)
Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection (Proceedings of the 24^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '24), 2024)
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates (Proceedings of the 24^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '24), 2024)
SMT-D: New Strategies for Portfolio-Based SMT Solving (Proceedings of the 24^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '24), 2024)
SGLang: Efficient Execution of Structured Language Model Programs (Advances in Neural Information Processing Systems 37 (NeurIPS 2024), 2024)

Edited Volumes

NASA Formal Methods: 9th International Symposium, NFM 2017 (2017)
Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2019 (2019)
Special Issue: Linearity and Special Issue: Selected Extended Papers of NFM 2017 (2019)

Journal Articles

An Industrially Effective Environment for Formal Hardware Verification (IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2005)
Design and Results of the 1^st Satisfiability Modulo Theories Competition (SMT-COMP 2005) (Journal of Automated Reasoning, 2005)
Translation and Run-Time Validation of Loop Transformations (Formal Methods in System Design, 2005)
Design and Results of the 2^nd Satisfiability Modulo Theories Competition (SMT-COMP 2006) (Formal Methods in System Design, 2007)
An Abstract Decision Procedure for a Theory of Inductive Data Types (Journal on Satisfiability, Boolean Modeling and Computation, 2007)
Design and Results of the 3^rd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2007) (International Journal on Artificial Intelligence Tools (IJAIT), 2008)
Solving Quantified Verification Conditions using Satisfiability Modulo Theories (Annals of Mathematics and Artificial Intelligence, 2009)
Being Careful about Theory Combination (Formal Methods in System Design, 2013)
6 Years of SMT-COMP (Journal of Automated Reasoning, 2013)
An Efficient SMT Solver for String Constraints (Formal Methods in System Design, 2016)
Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions (IEEE Design & Test, 2016)
Constraint solving for finite model finding in SMT solvers (Theory and Practice of Logic Programming, 2017)
Reasoning with Finite Sets and Cardinality Constraints in SMT (Logical Methods in Computer Science, 2018)
Logic Bug Detection and Localization Using Symbolic Quick Error Detection (IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018)
Refutation-Based Synthesis in SMT (Formal Methods in System Design, 2019)
On Solving Quantified Bit-Vectors using Invertibility Conditions (Formal Methods in System Design, 2021)
Algorithms for Verifying Deep Neural Networks (Foundations and Trends in Optimization, 2021)
Global optimization of objective functions represented by ReLU networks (Machine Learning, 2021)
Towards Satisfiability Modulo Parametric Bit-vectors (Journal of Automated Reasoning, 2021)
Reluplex: a Calculus for Reasoning about Deep Neural Networks (Formal Methods in System Design, 2022)
AHA: An Agile Approach to the Design of Course-Grained Reconfigurable Accelerators and Compilers (ACM Transactions on Embedded Computing Systems, 2022)
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (Logical Methods in Computer Science, 2022)
Polite Combination of Algebraic Datatypes (Journal of Automated Reasoning, 2022)
Scalable Verification of GNN-Based Job Schedulers (Proceedings of the ACM on Programming Languages, 2022)
Synthesising Programs with Non-trivial Constants (Journal of Automated Reasoning, 2023)
Combining Stable Infiniteness and (Strong) Politeness (Journal of Automated Reasoning, 2023)
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences (Journal of Automated Reasoning, 2023)
Generating and Exploiting Automated Reasoning Proof Certificates (Communications of the Association for Computing Machinery (CACM), 2023)
Identifying and Mitigating the Security Risks of Generative AI (Foundations and Trends in Privacy and Security, 2023)
QED and Symbolic QED: Dramatic Improvements in Pre-Silicon Verification and Post-Silicon Validation (Foundations and Trends in Integrated Circuits and Systems, 2024)
PEak: A Single Source of Truth for Hardware Design and Verification (ACM Transactions on Embedded Computing Systems, 2024)

Patents

Post-silicon validation and debug using symbolic quick error detection (2020)

Refereed Workshop Publications

A Generalization of Shostak's Method for Combining Decision Procedures (Proceedings of the 4^th International Workshop on Frontiers of Combining Systems (FroCoS '02), 2002)
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF (Proceedings of the 3^rd International Workshop on Logical Frameworks and Meta-Languages (LFM '02), 2002)
A Proof-Producing Boolean Search Engine (Proceedings of the 1^st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03), 2003)
Run-Time Validation of Speculative Optimizations using CVC (Proceedings of the 3^rd International Workshop on Run-time Verification (RV '03), 2003)
Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers (Proceedings of the 3^rd International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '04), 2005)
A Practical Approach to Partial Functions in CVC Lite (Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04), 2005)
Combining SAT Methods with Non-Clausal Decision Heuristics (Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04), 2005)
Validating More Loop Optimizations (Proceedings of the 4^th International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '05), 2005)
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite (Proceedings of the 3^rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05), 2006)
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (Combined Proceedings of the 4^th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '06) and the 1^st International Workshop on Probabilistic Automata and Logics (PaUL '06), 2007)
Comparing Proof Systems for Linear Real Arithmetic with LFSC (Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), 2010)
Sharing is Caring (Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), 2010)
The SMT-LIB Standard -- Version 2.0 (Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), 2010)
Exploring and Categorizing Error Spaces using BMC and SMT (Proceedings of the 9^th International Workshop on Satisfiability Modulo Theories (SMT '11), 2011)
Towards Proving the Adversarial Robustness of Deep Neural Networks (Proceedings of the First Workshop on Formal Verification of Autonomous Vehicles (FVAV '17), 2017)
Rewrites for SMT Solvers using Syntax-Guided Enumeration (Proceedings of the 16^th International Workshop on Satisfiability Modulo Theories (SMT '18), 2018)
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) (Proceedings of the Sixth Workshop on Proof eXchange for Theorem Proving (PxTP '19), 2019)
Verifying Deep-RL-Driven Systems (Proceedings of the 2019 Workshop on Network Meets AI & ML (NetAI '19), 2019)
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving (Extended Abstract) (Proceedings of the 18^th International Workshop on Satisfiability Modulo Theories (SMT '20), 2020)

Technical Reports

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (TR, 2005)
Splitting on Demand in SAT Modulo Theories (TR, 2006)
Points-to Analysis, Conditional Soundness, and Proving the Absence of Errors (TR, 2008)
Polite Theories Revisited (TR, 2010)
Design and Results of the 4^th Annual Satisfiability Modulo Theories Competition (SMT-COMP 2008) (TR, 2010)
Sharing is Caring: Combination of Theories (TR, 2011)
Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories (TR, 2014)
Provably Minimally-Distorted Adversarial Examples (2018)
Toward Scalable Verification for Safety-Critical Deep Networks (2018)
Global Optimization of Objective Functions Represented by ReLU Networks (2020)
Resources: A Safe Language Abstraction for Money (2020)
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection (2021)
FlexGen: High-Throughput Generative Inference of Large Language Models with a Single GPU (2023)
PEak: A Single Source of Truth for Hardware Design and Verification (2023)

Thesis

Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories (Ph.D. dissertation, 2003)

(This webpage was created with bibtex2web.)