Clark W. Barrett

According to our database1, Clark W. Barrett authored at least 118 papers between 1996 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2020
Smt-Switch: a solver-agnostic C++ API for SMT Solving.
CoRR, 2020

A Theoretical Framework for Symbolic Quick Error Detection.
CoRR, 2020

Parallelization Techniques for Verifying Neural Networks.
CoRR, 2020

Resources: A Safe Language Abstraction for Money.
CoRR, 2020

Verifying Recurrent Neural Networks using Invariant Inference.
CoRR, 2020

Partial Order Reduction for Deep Bug Finding in Synchronous Hardware.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Gap-free Processor Verification by S<sup>2</sup>QED and Property Generation.
Proceedings of the 2020 Design, Automation & Test in Europe Conference & Exhibition, 2020

The Move Prover.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

A Decision Procedure for String to Code Point Conversion.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Politeness for the Theory of Algebraic Datatypes.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019
Selected Extended Papers of NFM 2017: Preface.
J. Autom. Reasoning, 2019

Refutation-based synthesis in SMT.
Formal Methods Syst. Des., 2019

Simplifying Neural Networks with the Marabou Verification Engine.
CoRR, 2019

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract).
Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

CVC4SY for SyGuS-COMP 2019.
CoRR, 2019

Algorithms for Verifying Deep Neural Networks.
CoRR, 2019

Reports of the AAAI 2019 Spring Symposium Series.
AI Magazine, 2019

Verifying Deep-RL-Driven Systems.
Proceedings of the 2019 Workshop on Network Meets AI & ML, 2019

DRAT-based Bit-Vector Proofs in CVC4.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Agile SMT-Based Mapping for CGRAs with Restricted Routing Networks.
Proceedings of the 2019 International Conference on ReConFigurable Computing and FPGAs, 2019

G2SAT: Learning to Generate SAT Formulas.
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.
Proceedings of the International Conference on Computer-Aided Design, 2019

Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2019

Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2019

High-Level Abstractions for Simplifying Extended String Constraints in SMT.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

The Marabou Framework for Verification and Analysis of Deep Neural Networks.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Invertibility Conditions for Floating-Point Formulas.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Towards Bit-Width-Independent Proofs in SMT Solvers.
Proceedings of the Automated Deduction - CADE 27, 2019

Extending SMT Solvers to Higher-Order Logic.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
Satisfiability Modulo Theories.
Proceedings of the Handbook of Model Checking., 2018

Reasoning with Finite Sets and Cardinality Constraints in SMT.
Log. Methods Comput. Sci., 2018

CVC4 at the SMT Competition 2018.
CoRR, 2018

Toward Scalable Verification for Safety-Critical Deep Networks.
CoRR, 2018

EMME: A Formal Tool for ECMAScript Memory Model Evaluation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

p4pktgen: Automated Test Case Generation for P4 Programs.
Proceedings of the Symposium on SDN Research, 2018

CoSA: Integrated Verification for Agile Hardware Design.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Symbolic quick error detection using symbolic initial state for pre-silicon verification.
Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

Solving Quantified Bit-Vectors Using Invertibility Conditions.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Datatypes with Shared Selectors.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks.
Proceedings of the Automated Technology for Verification and Analysis, 2018

2017
Constraint solving for finite model finding in SMT solvers.
Theory Pract. Log. Program., 2017

Logic Bug Detection and Localization Using Symbolic Quick Error Detection.
CoRR, 2017

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

Ground-Truth Adversarial Examples.
CoRR, 2017

Towards Proving the Adversarial Robustness of Deep Neural Networks.
Proceedings of the Proceedings First Workshop on Formal Verification of Autonomous Vehicles, 2017

Partitioned Memory Models for Program Analysis.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Designing Theory Solvers with Extensions.
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.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Relational Constraint Solving in SMT.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
An efficient SMT solver for string constraints.
Formal Methods Syst. Des., 2016

Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions.
IEEE Des. Test, 2016

Efficient solving of string constraints for security analysis.
Proceedings of the Symposium and Bootcamp on the Science of Security, 2016

Lazy proofs for DPLL(T)-based SMT solvers.
Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4.
CoRR, 2015

Cascade - (Competition Contribution).
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.
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.
Proceedings of the 2015 IEEE International Test Conference, 2015

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Theory-Aided Model Checking of Concurrent Transition Systems.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Deciding Local Theory Extensions via E-matching.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Cascade 2.0.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

SMT: Where do we go from here?
Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014

A tour of CVC4: How it works, and how to use it.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Leveraging linear and mixed integer programming for SMT.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
6 Years of SMT-COMP.
J. Autom. Reasoning, 2013

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

Being careful about theory combination.
Formal Methods Syst. Des., 2013

Witness Runs for Counter Machines - (Abstract).
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Witness Runs for Counter Machines.
Proceedings of the Frontiers of Combining Systems, 2013

Simplex with sum of infeasibilities for SMT.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Quantifier Instantiation Techniques for Finite Model Finding in SMT.
Proceedings of the Automated Deduction - CADE-24, 2013

2011
Sharing Is Caring: Combination of Theories.
Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

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

2010
Polite Theories Revisited.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk).
Proceedings of the Hardware and Software: Verification and Testing, 2010

Verifying Low-Level Implementations of High-Level Datatypes.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Satisfiability Modulo Theories.
Proceedings of the Handbook of Satisfiability, 2009

Solving quantified verification conditions using satisfiability modulo theories.
Ann. Math. Artif. Intell., 2009

2008
Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007).
Int. J. Artif. Intell. Tools, 2008

Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors.
Proceedings of the Static Analysis, 15th International Symposium, 2008

2007
An Abstract Decision Procedure for a Theory of Inductive Data Types.
J. Satisf. Boolean Model. Comput., 2007

Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006).
Formal Methods Syst. Des., 2007

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types.
Electron. Notes Theor. Comput. Sci., 2007

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

2006
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite.
Electron. Notes Theor. Comput. Sci., 2006

Splitting on Demand in SAT Modulo Theories.
Proceedings of the Logic for Programming, 2006

cascade: C Assertion Checker and Deductive Engine.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005
An industrially effective environment for formal hardware verification.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2005

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

Translation and Run-Time Validation of Loop Transformations.
Formal Methods Syst. Des., 2005

Validating More Loop Optimizations.
Electron. Notes Theor. Comput. Sci., 2005

Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers.
Electron. Notes Theor. Comput. Sci., 2005

A Practical Approach to Partial Functions in CVC Lite.
Electron. Notes Theor. Comput. Sci., 2005

Combining SAT Methods with Non-Clausal Decision Heuristics.
Electron. Notes Theor. Comput. Sci., 2005

SMT-COMP: Satisfiability Modulo Theories Competition.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

TVOC: A Translation Validator for Optimizing Compilers.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations.
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.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
Run-Time Validation of Speculative Optimizations using CVC.
Electron. Notes Theor. Comput. Sci., 2003

2002
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF.
Electron. Notes Theor. Comput. Sci., 2002

A Generalization of Shostak's Method for Combining Decision Procedures.
Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

CVC: A Cooperating Validity Checker.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
A Decision Procedure for an Extensional Theory of Arrays.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000
A Framework for Cooperating Decision Procedures.
Proceedings of the Automated Deduction, 2000

1998
A Decision Procedure for Bit-Vector Arithmetic.
Proceedings of the 35th Conference on Design Automation, 1998

1996
Automatic Generation of Invariants in Processor Verification.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Validity Checking for Combinations of Theories with Equality.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996


  Loading...