2008 |
29 | EE | Christopher L. Conway,
Dennis Dams,
Kedar S. Namjoshi,
Clark Barrett:
Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors.
SAS 2008: 62-77 |
28 | EE | 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) |
2007 |
27 | EE | Yeting Ge,
Clark Barrett,
Cesare Tinelli:
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories.
CADE 2007: 167-182 |
26 | EE | Clark Barrett,
Cesare Tinelli:
CVC3.
CAV 2007: 298-302 |
25 | EE | 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) |
24 | EE | 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) |
23 | EE | Clark Barrett,
Igor Shikanian,
Cesare Tinelli:
An Abstract Decision Procedure for a Theory of Inductive Data Types.
JSAT 3(1-2): 21-46 (2007) |
2006 |
22 | EE | Nikhil Sethi,
Clark Barrett:
cascade: C Assertion Checker and Deductive Engine.
CAV 2006: 166-169 |
21 | EE | Clark Barrett,
Robert Nieuwenhuis,
Albert Oliveras,
Cesare Tinelli:
Splitting on Demand in SAT Modulo Theories.
LPAR 2006: 512-526 |
20 | EE | 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) |
2005 |
19 | EE | Clark W. Barrett,
Leonardo Mendonça de Moura,
Aaron Stump:
SMT-COMP: Satisfiability Modulo Theories Competition.
CAV 2005: 20-23 |
18 | EE | 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 |
17 | EE | 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) |
16 | EE | Ying Hu,
Clark W. Barrett,
Benjamin Goldberg,
Amir Pnueli:
Validating More Loop Optimizations.
Electr. Notes Theor. Comput. Sci. 141(2): 69-84 (2005) |
15 | EE | 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) |
14 | EE | 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) |
13 | EE | 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) |
2004 |
12 | EE | Clark W. Barrett,
Sergey Berezin:
CVC Lite: A New Implementation of the Cooperating Validity Checker Category B.
CAV 2004: 515-518 |
11 | EE | Ying Hu,
Clark W. Barrett,
Benjamin Goldberg:
Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations.
SEFM 2004: 281-289 |
2003 |
10 | EE | Clark W. Barrett,
Benjamin Goldberg,
Lenore D. Zuck:
Run-Time Validation of Speculative Optimizations using CVC.
Electr. Notes Theor. Comput. Sci. 89(2): (2003) |
2002 |
9 | EE | Clark W. Barrett,
David L. Dill,
Aaron Stump:
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.
CAV 2002: 236-249 |
8 | EE | Aaron Stump,
Clark W. Barrett,
David L. Dill:
CVC: A Cooperating Validity Checker.
CAV 2002: 500-504 |
7 | EE | Clark W. Barrett,
David L. Dill,
Aaron Stump:
A Generalization of Shostak's Method for Combining Decision Procedures.
FroCos 2002: 132-146 |
6 | EE | 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): (2002) |
2001 |
5 | | Aaron Stump,
Clark W. Barrett,
David L. Dill,
Jeremy R. Levitt:
A Decision Procedure for an Extensional Theory of Arrays.
LICS 2001: 29-37 |
2000 |
4 | | Clark W. Barrett,
David L. Dill,
Aaron Stump:
A Framework for Cooperating Decision Procedures.
CADE 2000: 79-98 |
1998 |
3 | EE | Clark W. Barrett,
David L. Dill,
Jeremy R. Levitt:
A Decision Procedure for Bit-Vector Arithmetic.
DAC 1998: 522-527 |
1996 |
2 | | Clark W. Barrett,
David L. Dill,
Jeremy R. Levitt:
Validity Checking for Combinations of Theories with Equality.
FMCAD 1996: 187-201 |
1 | | Jeffrey X. Su,
David L. Dill,
Clark W. Barrett:
Automatic Generation of Invariants in Processor Verification.
FMCAD 1996: 377-388 |