Clark Barrett's Publications

Also see publications by date


Contents:

Book Chapters

Satisfiability Modulo Theories (Handbook of Satisfiability, 2009)
Satisfiability Modulo Theories (Handbook of Model Checking, 2014)

Book Reviews

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

Conference Publications

Automatic Generation of Invariants in Processor Verification (Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96), 1996)
Validity Checking for Combinations of Theories with Equality (Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96), 1996)
A Decision Procedure for Bit-vector Arithmetic (Proceedings of the 35^th Design Automation Conference (DAC '98), 1998)
A Framework for Cooperating Decision Procedures (Proceedings of the 17^th International Conference on Computer-Aided Deduction (CADE '00), 2000)
A Decision Procedure for an Extensional Theory of Arrays (Proceedings of the 16^th IEEE Symposium on Logic in Computer Science (LICS '01), 2001)
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02), 2002)
CVC: A Cooperating Validity Checker (Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02), 2002)
CVC Lite: A New Implementation of the Cooperating Validity Checker (Proceedings of the 16^th International Conference on Computer Aided Verification (CAV '04), 2004)
Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations (Proceedings of the 2^nd IEEE International Conference on Software Engineering and Formal Methods (SEFM '04), 2004)
SMT-COMP: Satisfiability Modulo Theories Competition (Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05), 2005)
TVOC: A Translation Validator for Optimizing Compilers (Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05), 2005)
CASCADE: C Assertion Checker and Deductive Engine (Proceedings of the 18^th International Conference on Computer Aided Verification (CAV '06), 2006)
Splitting on Demand in SAT Modulo Theories (Proceedings of the 13^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '06), 2006)
Solving Quantified Verification Conditions using Satisfiability Modulo Theories (Proceedings of the 21^st International Conference on Automated Deduction (CADE '07), 2007)
CVC3 (Proceedings of the 19^th International Conference on Computer Aided Verification (CAV '07), 2007)
Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors (Proceedings of the 15^th International Static Analysis Symposium (SAS '08), 2008)
Verifying Low-Level Implementations of High-Level Datatypes (Proceedings of the 22^nd International Conference on Computer Aided Verification (CAV '10), 2010)
Polite Theories Revisited (Proceedings of the 17^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10), 2010)
CVC4 (Proceedings of the 23^rd International Conference on Computer Aided Verification (CAV '11), 2011)
Sharing is Caring: Combination of Theories (Proceedings of the 8^th International Symposium on Frontiers of Combining Systems (FroCoS '11), 2011)
Witness Runs for Counter Machines (Proceedings of the 9^th International Symposium on Frontiers of Combining Systems (FroCoS '13), 2013)
Simplex with Sum of Infeasibilities for SMT (Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), 2013)
The Design and Implementation of the Model Constructing Satisfiability Calculus (Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13), 2013)
Quantifier Instantiation Techniques for Finite Model Finding in SMT (Proceedings of the 24^th International Conference on Automated Deduction (CADE '13), 2013)
Cascade 2.0 (Proceedings of the 15^th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '14), 2014)
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14), 2014)
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14), 2014)

Journal Articles

An Industrially Effective Environment for Formal Hardware Verification (IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2005)
Design and Results of the 1^st Satisfiability Modulo Theories Competition (SMT-COMP 2005) (Journal of Automated Reasoning, 2005)
Translation and Run-Time Validation of Loop Transformations (Formal Methods in System Design, 2005)
Design and Results of the 2^nd Satisfiability Modulo Theories Competition (SMT-COMP 2006) (Formal Methods in System Design, 2007)
An Abstract Decision Procedure for a Theory of Inductive Data Types (Journal on Satisfiability, Boolean Modeling and Computation, 2007)
Design and Results of the 3^rd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2007) (International Journal on Artificial Intelligence Tools (IJAIT), 2008)
Solving Quantified Verification Conditions using Satisfiability Modulo Theories (Annals of Mathematics and Artificial Intelligence, 2009)
Being Careful about Theory Combination (Formal Methods in System Design, 2013)
6 Years of SMT-COMP (Journal of Automated Reasoning, 2013)

Patents

Reuse of learned information to simplify functional verification of a digital circuit (2007)

Refereed Workshop Publications

A Generalization of Shostak's Method for Combining Decision Procedures (Proceedings of the 4^th International Workshop on Frontiers of Combining Systems (FroCoS '02), 2002)
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF (Proceedings of the 3^rd International Workshop on Logical Frameworks and Meta-Languages (LFM '02), 2002)
A Proof-Producing Boolean Search Engine (Proceedings of the 1^st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03), 2003)
Run-Time Validation of Speculative Optimizations using CVC (Proceedings of the 3^rd International Workshop on Run-time Verification (RV '03), 2003)
Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers (Proceedings of the 3^rd International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '04), 2005)
A Practical Approach to Partial Functions in CVC Lite (Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04), 2005)
Combining SAT Methods with Non-Clausal Decision Heuristics (Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04), 2005)
Validating More Loop Optimizations (Proceedings of the 4^th International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '05), 2005)
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite (Proceedings of the 3^rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05), 2006)
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (Combined Proceedings of the 4^th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '06) and the 1^st International Workshop on Probabilistic Automata and Logics (PaUL '06), 2007)
Comparing Proof Systems for Linear Real Arithmetic with LFSC (Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), 2010)
Sharing is Caring (Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), 2010)
The SMT-LIB Standard -- Version 2.0 (Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10), 2010)
Exploring and Categorizing Error Spaces using BMC and SMT (Proceedings of the 9^th International Workshop on Satisfiability Modulo Theories (SMT '11), 2011)

Technical Reports

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (TR, 2005)
Splitting on Demand in SAT Modulo Theories (TR, 2006)
Points-to Analysis, Conditional Soundness, and Proving the Absence of Errors (TR, 2008)
Polite Theories Revisited (TR, 2010)
Design and Results of the 4^th Annual Satisfiability Modulo Theories Competition (SMT-COMP 2008) (TR, 2010)
Sharing is Caring: Combination of Theories (TR, 2011)
Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories (TR, 2014)

Thesis

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


(This webpage was created with bibtex2web.)