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, 2016)


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


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 DPLL(T) Solver for a Theory of Strings and Regular Expressions (Formal Methods in System Design, 2016)


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


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


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)


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)


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

(This webpage was created with bibtex2web.)