Clark W. Barrett, Ph.D. - Publications

Affiliations: 
2003 Stanford University, Palo Alto, CA 

36 high-probability publications. We are testing a new system for linking publications to authors. You can help! If you notice any inaccuracies, please sign in and mark papers as correct or incorrect matches. If you identify any major omissions or other inaccuracies in the publication list, please let us know.

Year Citation  Score
2019 Ekici B, Viswanathan A, Zohar Y, Barrett CW, Tinelli C. Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract) Arxiv: Logic in Computer Science. 301: 18-26. DOI: 10.4204/Eptcs.301.4  0.426
2015 Hadarean L, Barrett C, Reynolds A, Tinelli C, Deters M. Fine grained SMT proofs for the theory of fixed-width bit-vectors Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 9450: 340-355. DOI: 10.1007/978-3-662-48899-7_24  0.381
2015 Liang T, Tsiskaridze N, Reynolds A, Tinelli C, Barrett C. A decision procedure for regular membership and length constraints over unbounded strings Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 9322: 135-150. DOI: 10.1007/978-3-319-24246-0_9  0.428
2015 Bansal K, Reynolds A, King T, Barrett C, Wies T. Deciding local theory extensions via E-matching Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 9207: 87-105. DOI: 10.1007/978-3-319-21668-3_6  0.475
2014 Liang T, Reynolds A, Tinelli C, Barrett C, Deters M. A DPLL(T) theory solver for a theory of strings and regular expressions Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8559: 646-662. DOI: 10.1007/978-3-319-08867-9_43  0.38
2013 Barrett C. Decision procedures: An algorithmic point of view, by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008 Journal of Automated Reasoning. 51: 453-456. DOI: 10.1007/S10817-013-9295-4  0.53
2013 Barrett C, Deters M, De Moura L, Oliveras A, Stump A. 6 Years of SMT-COMP Journal of Automated Reasoning. 50: 243-277. DOI: 10.1007/S10817-012-9246-5  0.679
2013 Jovanović D, Barrett C. Being careful about theory combination Formal Methods in System Design. 42: 67-90. DOI: 10.1007/s10703-012-0159-z  0.354
2011 Jovanović D, Barrett C. Sharing is caring: Combination of theories Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6989: 195-210. DOI: 10.1007/978-3-642-24364-6_14  0.347
2011 Barrett C, Conway CL, Deters M, Hadarean L, Jovanović D, King T, Reynolds A, Tinelli C. CVC4 Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6806: 171-177. DOI: 10.1007/978-3-642-22110-1_14  0.348
2010 Jovanović D, Barrett C. Polite theories revisited Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6397: 402-416. DOI: 10.1007/978-3-642-16242-8-29  0.366
2009 Barrett C, Sebastiani R, Seshia SA, Tinelli C. Satisfiability modulo theories Frontiers in Artificial Intelligence and Applications. 185: 825-885. DOI: 10.3233/978-1-58603-929-5-825  0.459
2009 Ge Y, Barrett C, Tinelli C. Solving quantified verification conditions using satisfiability modulo theories Annals of Mathematics and Artificial Intelligence. 55: 101-122. DOI: 10.1007/S10472-009-9153-6  0.514
2008 Barrett C, Deters M, Oliveras A, Stump A. Design and results of the 3rd annual Satisfiability Modulo Theories Competition (SMT-COMP 2007) International Journal On Artificial Intelligence Tools. 17: 569-606. DOI: 10.1142/S0218213008004060  0.695
2007 Barrett CW, Shikanian I, Tinelli C. An Abstract Decision Procedure for a Theory of Inductive Data Types Journal On Satisfiability, Boolean Modeling and Computation. 3: 21-46. DOI: 10.3233/Sat190028  0.49
2007 Barrett C, Shikanian I, Tinelli C. An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types Electronic Notes in Theoretical Computer Science. 174: 23-37. DOI: 10.1016/J.Entcs.2006.11.037  0.502
2007 Barrett C, De Moura L, Stump A. Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) Formal Methods in System Design. 31: 221-239. DOI: 10.1007/s10703-007-0038-1  0.393
2007 Barrett C, Tinelli C. CVC3 Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4590: 298-302.  0.338
2006 Barrett C, Nieuwenhuis R, Oliveras A, Tinelli C. Splitting on demand in SAT Modulo theories Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4246: 512-526.  0.398
2005 Seger CJH, Jones RB, O'Leary JW, Melham T, Aagaard MD, Barrett C, Syme D. An industrially effective environment for formal hardware verification Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 24: 1381-1404. DOI: 10.1109/Tcad.2005.850814  0.385
2005 Hu Y, Barrett C, Goldberg B, Pnueli A. Validating more loop optimizations Electronic Notes in Theoretical Computer Science. 141: 69-84. DOI: 10.1016/J.Entcs.2005.02.044  0.352
2005 Goldberg B, Zuck L, Barrett C. Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers Electronic Notes in Theoretical Computer Science. 132: 53-71. DOI: 10.1016/J.Entcs.2005.01.030  0.348
2005 Barrett C, Donham J. Combining SAT Methods with Non-Clausal Decision Heuristics Electronic Notes in Theoretical Computer Science. 125: 3-12. DOI: 10.1016/J.Entcs.2004.09.042  0.409
2005 Berezin S, Barrett C, Shikanian I, Chechik M, Gurfinkel A, Dill DL. A practical approach to partial functions in CVC lite Electronic Notes in Theoretical Computer Science. 125: 13-23. DOI: 10.1016/J.Entcs.2004.06.064  0.571
2005 Barrett C, De Moura L, Stump A. Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) Journal of Automated Reasoning. 35: 373-390. DOI: 10.1007/S10817-006-9026-1  0.716
2005 Barrett C, De Moura L, Stump A. SMT-COMP: Satisfiability modulo theories competition Lecture Notes in Computer Science. 3576: 20-23.  0.349
2004 Barrett C, Berezin S. CVC lite: A new implementation of the cooperating validity checker. Category B Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 3114: 515-518.  0.416
2003 Barrett C, Goldberg B, Zuck L. Run-time validation of speculative optimizations using CVC Electronic Notes in Theoretical Computer Science. 89: 93-111. DOI: 10.1016/S1571-0661(04)81044-2  0.328
2002 Stump A, Barrett CW, Dill DL. Producing proofs from an arithmetic decision procedure in elliptical LF Electronic Notes in Theoretical Computer Science. 70: 31-43. DOI: 10.1016/S1571-0661(04)80504-8  0.714
2002 Barrett CW, Dill DL, Stump A. Checking satisfiability of first-order formulas by incremental translation to SAT Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2404: 236-249.  0.562
2002 Stump A, Barrett CW, Dill DL. CVC: A cooperating validity checker Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2404: 500-504.  0.67
2002 Barrett CW, Dill DL, Stump A. A generalization of shostak’s method for combining decision procedures Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2309: 132-146.  0.598
2001 Stump A, Barrett CW, Dill DL, Levitt J. A decision procedure for an extensional theory of arrays Proceedings - Symposium On Logic in Computer Science. 29-37.  0.65
2000 Barrett CW, Dill DL, Stump A. A framework for cooperating decision procedures Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science). 1831: 79-98.  0.615
1998 Barrett CW, Dill DL, Levitt JR. Decision procedure for bit-vector arithmetic Proceedings - Design Automation Conference. 522-527.  0.634
1996 Barrett C, Dill D, Levitt J. Validity checking for combinations of theories with equality Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1166: 187-201. DOI: 10.1007/BFb0031808  0.434
Show low-probability matches.