Clark W. Barrett

Proceedings of the 2023 IEEE Conference on Secure and Trustworthy Machine Learning, 2023

Towards Optimal Caching and Model Selection for Large Model Inference.

[BibT_eX]

[DOI]

Proceedings of the Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, 2023

H2O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models.

[BibT_eX]

[DOI]

Proceedings of the Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, 2023

VeriX: Towards Verified Explainability of Deep Neural Networks.

[BibT_eX]

[DOI]

Min Wu

Proceedings of the Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, 2023

Tighter Abstract Queries in Neural Network Verification.

[BibT_eX]

[DOI]

Elazar Cohen

Yizhak Yisrael Elboher

Guilherme Vicentin de Toledo

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

An Interactive SMT Tactic in Coq using Abductive Reasoning.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Soy: An Efficient MILP Solver for Piecewise-Affine Systems.

[BibT_eX]

[DOI]

IROS, 2023

Combining Finite Combination Properties: Finite Models and Busy Beavers.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

Formal Verification of Bit-Vector Invertibility Conditions in Coq.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning.

[BibT_eX]

[DOI]

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

Partitioning Strategies for Distributed SMT Solving.

[BibT_eX]

[DOI]

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

A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery.

[BibT_eX]

[DOI]

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

G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators.

[BibT_eX]

[DOI]

Keerthikumara Devarajegowda

Bihan Zhao

Guilherme Vicentin de Toledo

Brandon A. D'Agostino

Proceedings of the 60th ACM/IEEE Design Automation Conference, 2023

DNN Verification, Reachability, and the Exponential Function Problem.

[BibT_eX]

[DOI]

Proceedings of the 34th International Conference on Concurrency Theory, 2023

Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 29, 2023

APEX: A Framework for Automated Processing Element Design Space Exploration using Frequent Subgraph Analysis.

[BibT_eX]

[DOI]

Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2023

Convex Bounds on the Softmax Function with Applications to Robustness Verification.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Artificial Intelligence and Statistics, 2023

2022

Artifact for Paper Scalable Verification of GNN-Based Job Schedulers.

[BibT_eX]

[DOI]

Dataset, September, 2022

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.

[BibT_eX]

[DOI]

Aina Niemetz

Mathias Preiner

Dataset, May, 2022

Reluplex: a calculus for reasoning about deep neural networks.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., February, 2022

Artifact for Paper Efficient Neural Network Analysis with Sum-of-Infeasibilities.

[BibT_eX]

[DOI]

Dataset, February, 2022

Scalable verification of GNN-based job schedulers.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2022

Polite Combination of Algebraic Datatypes.

[BibT_eX]

[DOI]

Jane Lange

Pascal Fontaine

J. Autom. Reason., 2022

Proof-Stitch: Proof Combination for Divide and Conquer SAT Solvers.

[BibT_eX]

[DOI]

Abhishek Nair

Alex Ozdemir

CoRR, 2022

Bit-Precise Reasoning via Int-Blasting.

[BibT_eX]

[DOI]

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

Efficient Neural Network Analysis with Sum-of-Infeasibilities.

[BibT_eX]

[DOI]

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

cvc5: A Versatile and Industrial-Strength SMT Solver.

[BibT_eX]

[DOI]

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

On Optimizing Back-Substitution Methods for Neural Network Verification.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers.

[BibT_eX]

[DOI]

Abhishek Anil Nair

Alex Ozdemir

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Neural Network Verification with Proof Production.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Synthesizing Instruction Selection Rewrite Rules from RTL using SMT.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Even Faster Conflicts and Lazier Reductions for String Solvers.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.

[BibT_eX]

[DOI]

Aina Niemetz

Mathias Preiner

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Reasoning About Vectors Using an SMT Theory of Sequences.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks.

[BibT_eX]

[DOI]

Matan Ostrovsky

Proceedings of the Automated Technology for Verification and Analysis, 2022

2021

Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact).

[BibT_eX]

[DOI]

Dataset, February, 2021

Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

Towards Satisfiability Modulo Parametric Bit-vectors.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

Algorithms for Verifying Deep Neural Networks.

[BibT_eX]

[DOI]

Changliu Liu

Tomer Arnon

Christopher Lazarus

Christopher A. Strong

Found. Trends Optim., 2021

On solving quantified bit-vector constraints using invertibility conditions.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection.

[BibT_eX]

[DOI]

Karthik Ganesan

Srinivasa Shashank Nuthakki

CoRR, 2021

lazybvtoint at the SMT Competition 2020.

[BibT_eX]

[DOI]

CoRR, 2021

Automated Design Space Exploration of CGRA Processing Element Architectures using Frequent Subgraph Analysis.

[BibT_eX]

[DOI]

CoRR, 2021

Syntax-Guided Quantifier Instantiation.

[BibT_eX]

[DOI]

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

An SMT-Based Approach for Verifying Binarized Neural Networks.

[BibT_eX]

[DOI]

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

Smt-Switch: A Solver-Agnostic C++ API for SMT Solving.

[BibT_eX]

[DOI]

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

DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2021

Politeness for the Theory of Algebraic Datatypes (Extended Abstract).

[BibT_eX]

[DOI]

Jane Lange

Pascal Fontaine

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021

Automating System Configuration.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer Aided Design, 2021

SAT Solving in the Serverless Cloud.

[BibT_eX]

[DOI]

Alex Ozdemir

Proceedings of the Formal Methods in Computer Aided Design, 2021

Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer Aided Design, 2021

Pono: A Flexible and Extensible SMT-Based Model Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Politeness and Stable Infiniteness: Stronger Together.

[BibT_eX]

[DOI]

Andrew Reynolds

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Resources: A Safe Language Abstraction for Money.

[BibT_eX]

[DOI]

CoRR, 2020

Partial Order Reduction for Deep Bug Finding in Synchronous Hardware.

[BibT_eX]

[DOI]

Makai Mann

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

Smt-Switch: A Solver-agnostic C++ API for SMT Solving.

[BibT_eX]

[DOI]

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Simplifying Neural Networks Using Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 12th International Symposium, 2020

Parallelization Techniques for Verifying Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Reductions for Strings and Regular Expressions Revisited.

[BibT_eX]

[DOI]

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

A Theoretical Framework for Symbolic Quick Error Detection.

[BibT_eX]

[DOI]

Subhasish Mitra

Keerthikumara Devarajegowda

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Gap-free Processor Verification by S<sup>2</sup>QED and Property Generation.

[BibT_eX]

[DOI]

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

A-QED Verification of Hardware Accelerators.

[BibT_eX]

[DOI]

Proceedings of the 57th ACM/IEEE Design Automation Conference, 2020

Creating an Agile Hardware Design Flow.

[BibT_eX]

[DOI]

Proceedings of the 57th ACM/IEEE Design Automation Conference, 2020

The Move Prover.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

A Decision Procedure for String to Code Point Conversion.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Politeness for the Theory of Algebraic Datatypes.

[BibT_eX]

[DOI]

Jane Lange

Pascal Fontaine

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Verifying Recurrent Neural Networks Using Invariant Inference.

[BibT_eX]

[DOI]

Yuval Jacoby

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Selected Extended Papers of NFM 2017: Preface.

[BibT_eX]

[DOI]

Temesghen Kahsai

J. Autom. Reason., 2019

Refutation-based synthesis in SMT.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2019

Simplifying Neural Networks with the Marabou Verification Engine.

[BibT_eX]

[DOI]

CoRR, 2019

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

CVC4SY for SyGuS-COMP 2019.

[BibT_eX]

[DOI]

CoRR, 2019

Algorithms for Verifying Deep Neural Networks.

[BibT_eX]

[DOI]

CoRR, 2019

Reports of the AAAI 2019 Spring Symposium Series.

[BibT_eX]

[DOI]

AI Mag., 2019

Verifying Deep-RL-Driven Systems.

[BibT_eX]

[DOI]

Proceedings of the 2019 Workshop on Network Meets AI & ML, 2019

DRAT-based Bit-Vector Proofs in CVC4.

[BibT_eX]

[DOI]

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

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.

[BibT_eX]

[DOI]

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

Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks.

[BibT_eX]

[DOI]

Proceedings of the 2019 International Conference on ReConFigurable Computing and FPGAs, 2019

G2SAT: Learning to Generate SAT Formulas.

[BibT_eX]

[DOI]

Proceedings of the Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, 2019

Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper.

[BibT_eX]

[DOI]

Srinivasa Shashank Nuthakki

Karthik Ganesan

Makai Mann

Proceedings of the International Conference on Computer-Aided Design, 2019

Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study.

[BibT_eX]

[DOI]

Keerthikumara Devarajegowda

Sebastian Simon

Ralf Schnieder

Karthik Ganesan

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

Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking.

[BibT_eX]

[DOI]

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

High-Level Abstractions for Simplifying Extended String Constraints in SMT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

The Marabou Framework for Verification and Analysis of Deep Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Invertibility Conditions for Floating-Point Formulas.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Towards Bit-Width-Independent Proofs in SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

Extending SMT Solvers to Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Model Checking., 2018

Reasoning with Finite Sets and Cardinality Constraints in SMT.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2018

CVC4 at the SMT Competition 2018.

[BibT_eX]

[DOI]

CoRR, 2018

Toward Scalable Verification for Safety-Critical Deep Networks.

[BibT_eX]

[DOI]

CoRR, 2018

EMME: A Formal Tool for ECMAScript Memory Model Evaluation.

[BibT_eX]

[DOI]

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

p4pktgen: Automated Test Case Generation for P4 Programs.

[BibT_eX]

[DOI]

Proceedings of the Symposium on SDN Research, 2018

CoSA: Integrated Verification for Agile Hardware Design.

[BibT_eX]

[DOI]

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Symbolic quick error detection using symbolic initial state for pre-silicon verification.

[BibT_eX]

[DOI]

Srinivasa Shashank Nuthakki

Joakim Urdahl

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

Solving Quantified Bit-Vectors Using Invertibility Conditions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Datatypes with Shared Selectors.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2018

2017

Constraint solving for finite model finding in SMT solvers.

[BibT_eX]

[DOI]

Andrew Reynolds

Theory Pract. Log. Program., 2017

Logic Bug Detection and Localization Using Symbolic Quick Error Detection.

[BibT_eX]

[DOI]

CoRR, 2017

DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks.

[BibT_eX]

[DOI]

CoRR, 2017

Ground-Truth Adversarial Examples.

[BibT_eX]

[DOI]

CoRR, 2017

Towards Proving the Adversarial Robustness of Deep Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Workshop on Formal Verification of Autonomous Vehicles, 2017

Partitioned Memory Models for Program Analysis.

[BibT_eX]

[DOI]

Wei Wang

Thomas Wies

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

Designing Theory Solvers with Extensions.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods.

[BibT_eX]

[DOI]

Subhasish Mitra

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Relational Constraint Solving in SMT.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

An efficient SMT solver for string constraints.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2016

Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions.

[BibT_eX]

[DOI]

IEEE Des. Test, 2016

Efficient solving of string constraints for security analysis.

[BibT_eX]

[DOI]

Proceedings of the Symposium and Bootcamp on the Science of Security, 2016

Lazy proofs for DPLL(T)-based SMT solvers.

[BibT_eX]

[DOI]

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

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4.

[BibT_eX]

[DOI]

CoRR, 2015

Cascade - (Competition Contribution).

[BibT_eX]

[DOI]

Wei Wang

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

Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors.

[BibT_eX]

[DOI]

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

A structured approach to post-silicon validation and debug using symbolic quick error detection.

[BibT_eX]

[DOI]

Proceedings of the 2015 IEEE International Test Conference, 2015

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Theory-Aided Model Checking of Concurrent Transition Systems.

[BibT_eX]

[DOI]

David Harel

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

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Deciding Local Theory Extensions via E-matching.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Cascade 2.0.

[BibT_eX]

[DOI]

Wei Wang

Thomas Wies

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

SMT: Where do we go from here?

[BibT_eX]

[DOI]

Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014

Leveraging Linear and Mixed Integer Programming for SMT.

[BibT_eX]

[DOI]

Tim King

Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014

A tour of CVC4: How it works, and how to use it.

[BibT_eX]

[DOI]

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

A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.

[BibT_eX]

[DOI]

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

A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors.

[BibT_eX]

[DOI]

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

2013

6 Years of SMT-COMP.

[BibT_eX]

[DOI]

Morgan Deters

Albert Oliveras

J. Autom. Reason., 2013

"Decision Procedures: An Algorithmic Point of View, " by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

Being careful about theory combination.

[BibT_eX]

[DOI]

Dejan Jovanovic

Formal Methods Syst. Des., 2013

Witness Runs for Counter Machines - (Abstract).

[BibT_eX]

[DOI]

Stéphane Demri

Morgan Deters

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Witness Runs for Counter Machines.

[BibT_eX]

[DOI]

Stéphane Demri

Morgan Deters

Proceedings of the Frontiers of Combining Systems, 2013

Simplex with sum of infeasibilities for SMT.

[BibT_eX]

[DOI]

Tim King

Bruno Dutertre

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

Quantifier Instantiation Techniques for Finite Model Finding in SMT.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

2011

Sharing Is Caring: Combination of Theories.

[BibT_eX]

[DOI]

Dejan Jovanovic

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

CVC4.

[BibT_eX]

[DOI]

Christopher L. Conway

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

2010

Polite Theories Revisited.

[BibT_eX]

[DOI]

Dejan Jovanovic

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

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk).

[BibT_eX]

[DOI]

Silvio Ranise

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

Verifying Low-Level Implementations of High-Level Datatypes.

[BibT_eX]

[DOI]

Christopher L. Conway

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability, 2009

Solving quantified verification conditions using satisfiability modulo theories.

[BibT_eX]

[DOI]

Yeting Ge

Ann. Math. Artif. Intell., 2009

2008

Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007).

[BibT_eX]

[DOI]

Int. J. Artif. Intell. Tools, 2008

Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors.

[BibT_eX]

[DOI]

Christopher L. Conway

Dennis Dams

Kedar S. Namjoshi

Proceedings of the Static Analysis, 15th International Symposium, 2008

2007

An Abstract Decision Procedure for a Theory of Inductive Data Types.

[BibT_eX]

[DOI]

Igor Shikanian

J. Satisf. Boolean Model. Comput., 2007

Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006).

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2007

CVC3.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types.

[BibT_eX]

[DOI]

Igor Shikanian

Proceedings of the Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), 2006

Splitting on Demand in SAT Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

cascade: C Assertion Checker and Deductive Engine.

[BibT_eX]

[DOI]

Nikhil Sethi

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

An industrially effective environment for formal hardware verification.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2005

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005).

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Translation and Run-Time Validation of Loop Transformations.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2005

Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite.

[BibT_eX]

[DOI]

Sean McLaughlin

Yeting Ge

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Validating More Loop Optimizations.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Workshop on Compiler Optimization meets Compiler Verification, 2005

SMT-COMP: Satisfiability Modulo Theories Competition.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

TVOC: A Translation Validator for Optimizing Compilers.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers.

[BibT_eX]

[DOI]

Benjamin Goldberg

Lenore D. Zuck

Proceedings of the 3rd International Workshop on Compiler Optimization Meets Compiler Verification, 2004

A Practical Approach to Partial Functions in CVC Lite.

[BibT_eX]

[DOI]

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Combining SAT Methods with Non-Clausal Decision Heuristics.

[BibT_eX]

[DOI]

Jacob Donham

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations.

[BibT_eX]

[DOI]

Ying Hu

Benjamin Goldberg

Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

CVC Lite: A New Implementation of the Cooperating Validity Checker Category B.

[BibT_eX]

[DOI]

Sergey Berezin

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Run-Time Validation of Speculative Optimizations using CVC.

[BibT_eX]

[DOI]

Benjamin Goldberg

Lenore D. Zuck

Proceedings of the Third Workshop on Run-time Verification, 2003

2002

Checking validity of quantifier-free formulas in combinations of first-order theories.

[BibT_eX]

[DOI]

PhD thesis, 2002

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Logical Frameworks and Meta-Languages, 2002

A Generalization of Shostak's Method for Combining Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

CVC: A Cooperating Validity Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

A Decision Procedure for an Extensional Theory of Arrays.

[BibT_eX]

[DOI]

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000

A Framework for Cooperating Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2000

1998

A Decision Procedure for Bit-Vector Arithmetic.

[BibT_eX]

[DOI]

Jeremy R. Levitt

Proceedings of the 35th Conference on Design Automation, 1998

1996

Automatic Generation of Invariants in Processor Verification.

[BibT_eX]

[DOI]

Jeffrey X. Su

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Validity Checking for Combinations of Theories with Equality.

[BibT_eX]

[DOI]