Clark W. Barrett

Dejan Jovanovic, Clark Barrett: Being careful about theory combination. Formal Methods in System Design 42(1): 67-90 (2013)

Clark Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump: 6 Years of SMT-COMP. J. Autom. Reasoning 50(3): 243-277 (2013)

Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli: CVC4. CAV 2011: 171-177

Dejan Jovanovic, Clark Barrett: Sharing Is Caring: Combination of Theories. FroCoS 2011: 195-210

Christopher L. Conway, Clark Barrett: Verifying Low-Level Implementations of High-Level Datatypes. CAV 2010: 306-320

Clark Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli: The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference 2010: 3

Dejan Jovanovic, Clark Barrett: Polite Theories Revisited. LPAR (Yogyakarta) 2010: 402-416

Yeting Ge, Clark W. Barrett, Cesare Tinelli: Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1-2): 101-122 (2009)

Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli: Satisfiability Modulo Theories. Handbook of Satisfiability 2009: 825-885

Clark Barrett, Morgan Deters, Albert Oliveras, Aaron Stump: Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). International Journal on Artificial Intelligence Tools 17(4): 569-606 (2008)

Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark Barrett: Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors. SAS 2008: 62-77

Clark Barrett, Igor Shikanian, Cesare Tinelli: An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. Electr. Notes Theor. Comput. Sci. 174(8): 23-37 (2007)

Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump: Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods in System Design 31(3): 221-239 (2007)

Clark Barrett, Igor Shikanian, Cesare Tinelli: An Abstract Decision Procedure for a Theory of Inductive Data Types. JSAT 3(1-2): 21-46 (2007)

Yeting Ge, Clark Barrett, Cesare Tinelli: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. CADE 2007: 167-182

Clark Barrett, Cesare Tinelli: CVC3. CAV 2007: 298-302

Sean McLaughlin, Clark Barrett, Yeting Ge: Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. Electr. Notes Theor. Comput. Sci. 144(2): 43-51 (2006)

Nikhil Sethi, Clark Barrett: cascade: C Assertion Checker and Deductive Engine. CAV 2006: 166-169

Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526

Clark Barrett, Jacob Donham: Combining SAT Methods with Non-Clausal Decision Heuristics. Electr. Notes Theor. Comput. Sci. 125(3): 3-12 (2005)

Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill: A Practical Approach to Partial Functions in CVC Lite. Electr. Notes Theor. Comput. Sci. 125(3): 13-23 (2005)

Benjamin Goldberg, Lenore D. Zuck, Clark W. Barrett: Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. Electr. Notes Theor. Comput. Sci. 132(1): 53-71 (2005)

Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli: Validating More Loop Optimizations. Electr. Notes Theor. Comput. Sci. 141(2): 69-84 (2005)

Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu: Translation and Run-Time Validation of Loop Transformations. Formal Methods in System Design 27(3): 335-360 (2005)

Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump: Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reasoning 35(4): 373-390 (2005)

Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark Aagaard, Clark Barrett, Don Syme: An industrially effective environment for formal hardware verification. IEEE Trans. on CAD of Integrated Circuits and Systems 24(9): 1381-1405 (2005)

Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump: SMT-COMP: Satisfiability Modulo Theories Competition. CAV 2005: 20-23

Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck: TVOC: A Translation Validator for Optimizing Compilers. CAV 2005: 291-295

Clark W. Barrett, Sergey Berezin: CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. CAV 2004: 515-518

Ying Hu, Clark W. Barrett, Benjamin Goldberg: Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations. SEFM 2004: 281-289

Clark W. Barrett, Benjamin Goldberg, Lenore D. Zuck: Run-Time Validation of Speculative Optimizations using CVC. Electr. Notes Theor. Comput. Sci. 89(2): 89-107 (2003)

Aaron Stump, Clark W. Barrett, David L. Dill: Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. Electr. Notes Theor. Comput. Sci. 70(2): 29-41 (2002)

Clark W. Barrett, David L. Dill, Aaron Stump: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV 2002: 236-249

Aaron Stump, Clark W. Barrett, David L. Dill: CVC: A Cooperating Validity Checker. CAV 2002: 500-504

Clark W. Barrett, David L. Dill, Aaron Stump: A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS 2002: 132-146

Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt: A Decision Procedure for an Extensional Theory of Arrays. LICS 2001: 29-37

Clark W. Barrett, David L. Dill, Aaron Stump: A Framework for Cooperating Decision Procedures. CADE 2000: 79-98

Clark W. Barrett, David L. Dill, Jeremy R. Levitt: A Decision Procedure for Bit-Vector Arithmetic. DAC 1998: 522-527

Clark W. Barrett, David L. Dill, Jeremy R. Levitt: Validity Checking for Combinations of Theories with Equality. FMCAD 1996: 187-201

Jeffrey X. Su, David L. Dill, Clark W. Barrett: Automatic Generation of Invariants in Processor Verification. FMCAD 1996: 377-388