Clark Barrett's Publications
Also see publications by date
Contents:

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)


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


Automatic Generation of Invariants in Processor Verification (Proceedings of the 1^st International Conference on Formal Methods In ComputerAided Design (FMCAD '96), 1996)


Validity Checking for Combinations of Theories with Equality (Proceedings of the 1^st International Conference on Formal Methods In ComputerAided Design (FMCAD '96), 1996)


A Decision Procedure for Bitvector 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 ComputerAided 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 FirstOrder 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)


SMTCOMP: 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 LowLevel Implementations of HighLevel 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 ComputerAided 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 ComputerAided 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 Bitvectors (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 ComputerAided 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 Ematching (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)


TheoryAided Model Checking of Concurrent Transition Systems (Proceedings of the 15^th International Conference on Formal Methods In ComputerAided Design (FMCAD '15), 2015)


A Structured Approach to PostSilicon Validation and Debug using Symbolic Quick Error Detection (Proceedings of the 42^nd International Test Conference (ITC '15), 2015)


Finegrained SMT Proofs for the Theory of Fixedwidth Bitvectors (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 ComputerAided 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 ContextDependent Simplification (Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), 2017)


EQED: Electrical Bug Localization During PostSilicon 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 PlugIn 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 presilicon 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 BitVectors using Invertibility Conditions (Proceedings of the 30^th International Conference on Computer Aided Verification (CAV '18), 2018)


DeepSafe: A Datadriven 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 ComputerAided 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 Presilicon Verification for Automotive Microcontroller Cores: Industrial Case Study (Proceedings of the 2019 Design, Automation and Test in Europe (DATE '19), 2019)


HighLevel 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 FloatingPoint Formulas (Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), 2019)


SyntaxGuided 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 SyntaxGuided Synthesis (Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), 2019)


DRATbased BitVector Proofs in CVC4 (Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19), 2019)


Extending SMT Solvers to HigherOrder Logic (Proceedings of the 27^th International Conference on Automated Deduction (CADE '19), 2019)


Towards BitWidthIndependent 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 ComputerAided Design (ICCAD '19), 2019)


Agile SMTBased 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)


GapFree 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 DomainSpecific Language for Metaprogramming Portable Hardware Verification Components (Proceedings of the 32^nd International Conference on Computer Aided Verification (CAV '20), 2020)


AQED 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 ComputerAided Design (FMCAD '20), 2020)


Parallelization Techniques for Verifying Neural Networks (Proceedings of the 20^th International Conference on Formal Methods In ComputerAided Design (FMCAD '20), 2020)


Reductions for Strings and Regular Expressions Revisited (Proceedings of the 20^th International Conference on Formal Methods In ComputerAided 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 SMTBased 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)


CounterexampleGuided 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)


SyntaxGuided 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 SMTbased Model Checker (Proceedings of the 33^rd International Conference on Computer Aided Verification (CAV '21), 2021)


SmtSwitch: A SolverAgnostic 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 ComputerAided Design (FMCAD '21), 2021)


Scaling Up Hardware Accelerator Verification using AQED with Functional Decomposition (Proceedings of the 21^st International Conference on Formal Methods In ComputerAided Design (FMCAD '21), 2021)


SAT Solving in the Serverless Cloud (Proceedings of the 21^st International Conference on Formal Methods In ComputerAided Design (FMCAD '21), 2021)


BitPrecise Reasoning via IntBlasting (Proceedings of the 23^rd International Conference on Verification, Model Checking, and Abstract Interpretion (VMCAI '22), 2022)


Efficient Neural Network Analysis with SumofInfeasibilities (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 IndustrialStrength 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 IndustrialStrength 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 AbstractionRefinement 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 ComputerAided Design (FMCAD '22), 2022)


On Optimizing BackSubstitution Methods for Neural Network Verification (Proceedings of the 22^nd International Conference on Formal Methods In ComputerAided Design (FMCAD '22), 2022)


ProofStitch: Proof Combination for DivideandConquer SAT Solvers (Proceedings of the 22^nd International Conference on Formal Methods In ComputerAided Design (FMCAD '22), 2022)


Reconstructing FineGrained Proofs of Rewrites Using a DomainSpecific Language (Proceedings of the 22^nd International Conference on Formal Methods In ComputerAided Design (FMCAD '22), 2022)


Synthesizing Instruction Selection Rewrite Rules from RTL using SMT (Proceedings of the 22^nd International Conference on Formal Methods In ComputerAided Design (FMCAD '22), 2022)


Toward Certified Robustness Against RealWorld 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 FiniteFieldBlasting (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)


GQED: Generalized QED Presilicon Verification beyond NonInterfering 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 BitVector 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 ComputerAided 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 ComputerAided Design (FMCAD '23), 2023)


Partitioning Strategies for Distributed SMT Solving (Proceedings of the 23^rd International Conference on Formal Methods In ComputerAided Design (FMCAD '23), 2023)


Soy: An Efficient MILP Solver for PiecewiseAffine Systems (2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS '23), 2023)


H_2O: HeavyHitter 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)


NASA Formal Methods: 9th International Symposium, NFM 2017 (2017)


Proceedings of Formal Methods in ComputerAided Design, FMCAD 2019 (2019)


Special Issue: Linearity and Special Issue: Selected Extended Papers of NFM 2017 (2019)


An Industrially Effective Environment for Formal Hardware Verification (IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems, 2005)


Design and Results of the 1^st Satisfiability Modulo Theories Competition (SMTCOMP 2005) (Journal of Automated Reasoning, 2005)


Translation and RunTime Validation of Loop Transformations (Formal Methods in System Design, 2005)


Design and Results of the 2^nd Satisfiability Modulo Theories Competition (SMTCOMP 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 (SMTCOMP 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 SMTCOMP (Journal of Automated Reasoning, 2013)


An Efficient SMT Solver for String Constraints (Formal Methods in System Design, 2016)


Symbolic Quick Error Detection for PreSilicon and PostSilicon 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 ComputerAided Design of Integrated Circuits and Systems, 2018)


RefutationBased Synthesis in SMT (Formal Methods in System Design, 2019)


On Solving Quantified BitVectors 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 Bitvectors (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 CourseGrained Reconfigurable Accelerators and Compilers (ACM Transactions on Embedded Computing Systems, 2022)


CounterexampleGuided 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 GNNBased Job Schedulers (Proceedings of the ACM on Programming Languages, 2022)


Synthesising Programs with Nontrivial 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)


Postsilicon validation and debug using symbolic quick error detection (2020)


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 MetaLanguages (LFM '02), 2002)


A ProofProducing Boolean Search Engine (Proceedings of the 1^st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03), 2003)


RunTime Validation of Speculative Optimizations using CVC (Proceedings of the 3^rd International Workshop on Runtime 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 NonClausal 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 HOLLight 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 SMTLIB 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 SyntaxGuided Enumeration (Proceedings of the 16^th International Workshop on Satisfiability Modulo Theories (SMT '18), 2018)


Verifying Bitvector Invertibility Conditions in Coq (Extended Abstract) (Proceedings of the Sixth Workshop on Proof eXchange for Theorem Proving (PxTP '19), 2019)


Verifying DeepRLDriven Systems (Proceedings of the 2019 Workshop on Network Meets AI & ML (NetAI '19), 2019)


SmtSwitch: A SolverAgnostic C++ API for SMT Solving (Extended Abstract) (Proceedings of the 18^th International Workshop on Satisfiability Modulo Theories (SMT '20), 2020)


An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (TR, 2005)


Splitting on Demand in SAT Modulo Theories (TR, 2006)


Pointsto 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 (SMTCOMP 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 MinimallyDistorted Adversarial Examples (2018)


Toward Scalable Verification for SafetyCritical Deep Networks (2018)


Global Optimization of Objective Functions Represented by ReLU Networks (2020)


Resources: A Safe Language Abstraction for Money (2020)


Effective PreSilicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection (2021)


FlexGen: HighThroughput Generative Inference of Large Language Models with a Single GPU (2023)


PEak: A Single Source of Truth for Hardware Design and Verification (2023)


Checking Validity of QuantifierFree Formulas in Combinations of FirstOrder Theories (Ph.D. dissertation, 2003)

(This webpage was created with bibtex2web.)