Clark W. Barrett

Orcid: 0000-0002-9522-3084

Affiliations:
  • Stanford University, Computer Science Department, CA, USA
  • New York University, Department of Computer Science, NY, USA
  • Stanford University, Computer Systems Laboratory, CA, USA


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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks.
CoRR, 2024

Towards Efficient Verification of Quantized Neural Networks.
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023
Combining Stable Infiniteness and (Strong) Politeness.
J. Autom. Reason., December, 2023

Global optimization of objective functions represented by ReLU networks.
Mach. Learn., October, 2023

Generating and Exploiting Automated Reasoning Proof Certificates.
Commun. ACM, October, 2023

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences.
J. Autom. Reason., September, 2023

Synthesising Programs with Non-trivial Constants.
J. Autom. Reason., June, 2023

AHA: An Agile Approach to the Design of Coarse-Grained Reconfigurable Accelerators and Compilers.
ACM Trans. Embed. Comput. Syst., March, 2023

Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs).
IACR Cryptol. ePrint Arch., 2023

Satisfiability Modulo Finite Fields.
IACR Cryptol. ePrint Arch., 2023

Identifying and Mitigating the Security Risks of Generative AI.
Found. Trends Priv. Secur., 2023

Efficiently Programming Large Language Models using SGLang.
CoRR, 2023

Clover: Closed-Loop Verifiable Code Generation.
CoRR, 2023

Lemur: Integrating Large Language Models in Automated Program Verification.
CoRR, 2023

Identifying and Mitigating the Security Risks of Generative AI.
CoRR, 2023

PEak: A Single Source of Truth for Hardware Design and Verification.
CoRR, 2023

H<sub>2</sub>O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models.
CoRR, 2023

On Optimal Caching and Model Multiplexing for Large Model Inference.
CoRR, 2023

High-throughput Generative Inference of Large Language Models with a Single GPU.
CoRR, 2023

Automatic Verification of SMT Rewrites in Isabelle/HOL.
Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

Towards Optimal Caching and Model Selection for Large Model Inference.
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.
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.
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.
Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

An Interactive SMT Tactic in Coq using Abductive Reasoning.
Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

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

Combining Finite Combination Properties: Finite Models and Busy Beavers.
Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

Formal Verification of Bit-Vector Invertibility Conditions in Coq.
Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

Partitioning Strategies for Distributed SMT Solving.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators.
Proceedings of the 60th ACM/IEEE Design Automation Conference, 2023

DNN Verification, Reachability, and the Exponential Function Problem.
Proceedings of the 34th International Conference on Concurrency Theory, 2023

Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness.
Proceedings of the Automated Deduction - CADE 29, 2023

APEX: A Framework for Automated Processing Element Design Space Exploration using Frequent Subgraph Analysis.
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.
Proceedings of the International Conference on Artificial Intelligence and Statistics, 2023

2022
Reluplex: a calculus for reasoning about deep neural networks.
Formal Methods Syst. Des., February, 2022

Scalable verification of GNN-based job schedulers.
Proc. ACM Program. Lang., 2022

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays.
Log. Methods Comput. Sci., 2022

Polite Combination of Algebraic Datatypes.
J. Autom. Reason., 2022

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

Toward Certified Robustness Against Real-World Distribution Shifts.
CoRR, 2022

Bit-Precise Reasoning via Int-Blasting.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

Efficient Neural Network Analysis with Sum-of-Infeasibilities.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

cvc5: A Versatile and Industrial-Strength SMT Solver.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

On Optimizing Back-Substitution Methods for Neural Network Verification.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Neural Network Verification with Proof Production.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Synthesizing Instruction Selection Rewrite Rules from RTL using SMT.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Even Faster Conflicts and Lazier Reductions for String Solvers.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Reasoning About Vectors Using an SMT Theory of Sequences.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description).
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks.
Proceedings of the Automated Technology for Verification and Analysis, 2022

2021
Satisfiability Modulo Theories.
Proceedings of the Handbook of Satisfiability - Second Edition, 2021

Towards Satisfiability Modulo Parametric Bit-vectors.
J. Autom. Reason., 2021

Algorithms for Verifying Deep Neural Networks.
Found. Trends Optim., 2021

On solving quantified bit-vector constraints using invertibility conditions.
Formal Methods Syst. Des., 2021

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

lazybvtoint at the SMT Competition 2020.
CoRR, 2021

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

Syntax-Guided Quantifier Instantiation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

An SMT-Based Approach for Verifying Binarized Neural Networks.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Smt-Switch: A Solver-Agnostic C++ API for SMT Solving.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers.
Proceedings of the Computer Safety, Reliability, and Security, 2021

Politeness for the Theory of Algebraic Datatypes (Extended Abstract).
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021

Automating System Configuration.
Proceedings of the Formal Methods in Computer Aided Design, 2021

SAT Solving in the Serverless Cloud.
Proceedings of the Formal Methods in Computer Aided Design, 2021

Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition.
Proceedings of the Formal Methods in Computer Aided Design, 2021

Pono: A Flexible and Extensible SMT-Based Model Checker.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Politeness and Stable Infiniteness: Stronger Together.
Proceedings of the Automated Deduction - CADE 28, 2021

2020
Resources: A Safe Language Abstraction for Money.
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

Smt-Switch: A Solver-agnostic C++ API for SMT Solving.
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.
Proceedings of the NASA Formal Methods - 12th International Symposium, 2020

Parallelization Techniques for Verifying Neural Networks.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Reductions for Strings and Regular Expressions Revisited.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

A Theoretical Framework for Symbolic Quick Error Detection.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 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

A-QED Verification of Hardware Accelerators.
Proceedings of the 57th ACM/IEEE Design Automation Conference, 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

Verifying Recurrent Neural Networks Using Invariant Inference.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
Selected Extended Papers of NFM 2017: Preface.
J. Autom. Reason., 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 Mag., 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. Reason., 2013

"Decision Procedures: An Algorithmic Point of View, " by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008.
J. Autom. Reason., 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

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

2006
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types.
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.
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. Comput. Aided Des. Integr. Circuits Syst., 2005

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

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

Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite.
Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Validating More Loop Optimizations.
Proceedings of the Fourth International Workshop on Compiler Optimization meets Compiler Verification, 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
Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers.
Proceedings of the 3rd International Workshop on Compiler Optimization Meets Compiler Verification, 2004

A Practical Approach to Partial Functions in CVC Lite.
Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Combining SAT Methods with Non-Clausal Decision Heuristics.
Proceedings of the Selected Papers from the Workshops on Disproving, 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.
Proceedings of the Third Workshop on Run-time Verification, 2003

2002
Checking validity of quantifier-free formulas in combinations of first-order theories.
PhD thesis, 2002

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF.
Proceedings of the International Workshop on Logical Frameworks and Meta-Languages, 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...