Clark W. Barrett, Ph.D. - Publications

Affiliations: 
2003 Stanford University, Palo Alto, CA 

53 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
2015 Lin D, Singh E, Barrett C, Mitra S. A structured approach to post-silicon validation and debug using symbolic quick error detection Proceedings - International Test Conference. 2015. DOI: 10.1109/TEST.2015.7342397  0.36
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.36
2015 Wang W, Barrett C. Cascade (Competition contribution) Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 9035: 420-422. DOI: 10.1007/978-3-662-46681-0_33  0.36
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.36
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.36
2015 Reynolds A, Deters M, Kuncak V, Tinelli C, Barrett C. Counterexample-guided quantifier instantiation for synthesis in SMT Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 9207: 198-216. DOI: 10.1007/978-3-319-21668-3_12  0.36
2014 King T, Barrett C, Tinelli C. Leveraging linear and mixed integer programming for SMT 2014 Formal Methods in Computer-Aided Design, Fmcad 2014. 139-146. DOI: 10.1109/FMCAD.2014.6987606  0.36
2014 Wang W, Barrett C, Wies T. Cascade 2.0 Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8318: 142-160. DOI: 10.1007/978-3-642-54013-4_9  0.36
2014 Hadarean L, Bansal K, Jovanović D, Barrett C, Tinelli C. A tale of two solvers: Eager and lazy approaches to bit-vectors Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8559: 680-695. DOI: 10.1007/978-3-319-08867-9_45  0.36
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.36
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.36
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.36
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.36
2013 Barrett C, Demri S, Deters M. Witness runs for counter machines Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8152: 120-150. DOI: 10.1007/978-3-642-40885-4_9  0.36
2013 Barrett C, Demri S, Deters M. Witness runs for counter machines (abstract) Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8123: 1-4. DOI: 10.1007/978-3-642-40537-2_1  0.36
2013 Reynolds A, Tinelli C, Goel A, Krstić S, Deters M, Barrett C. Quantifier instantiation techniques for finite model finding in SMT Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 7898: 377-391. DOI: 10.1007/978-3-642-38574-2_26  0.36
2013 King T, Barrett C, Dutertre B. Simplex with sum of infeasibilities for SMT 2013 Formal Methods in Computer-Aided Design, Fmcad 2013. 189-196.  0.36
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.36
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.36
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.36
2010 Conway CL, Barrett C. Verifying low-level implementations of high-level datatypes Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 6174: 306-320. DOI: 10.1007/978-3-642-14295-6_28  0.36
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.36
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.36
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.36
2008 Conway CL, Dams D, Namjoshi KS, Barrett C. Pointer analysis, conditional soundness, and proving the absence of errors Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 5079: 62-77. DOI: 10.1007/978-3-540-69166-2_5  0.36
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.36
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.36
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.36
2006 McLaughlin S, Barrett C, Ge Y. Cooperating theorem provers: A case study combining HOL-light and CVC lite Electronic Notes in Theoretical Computer Science. 144: 43-51. DOI: 10.1016/j.entcs.2005.12.005  0.36
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.36
2006 Sethi N, Barrett C. Cascade: C assertion checker and deductive engine Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4144: 166-169.  0.36
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.36
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.36
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.36
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.36
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.36
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.36
2005 Zuck L, Pnueli A, Goldberg B, Barrett C, Fang Y, Hu Y. Translation and run-time validation of loop transformations Formal Methods in System Design. 27: 335-360. DOI: 10.1007/s10703-005-3402-z  0.36
2005 Barrett C, Fang Y, Goldberg B, Hu Y, Pnueli A, Zuck L. TVOC: A translation validator for optimizing compilers Lecture Notes in Computer Science. 3576: 291-295.  0.36
2005 Barrett C, De Moura L, Stump A. SMT-COMP: Satisfiability modulo theories competition Lecture Notes in Computer Science. 3576: 20-23.  0.36
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.36
2004 Hu Y, Barrett C, Goldberg B. Theory and algorithms for the generation and validation of speculative loop optimizations Proceedings of the Second International Conference On Software Engineering and Formal Methods. Sefm 2004. 281-289.  0.36
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.36
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.36
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.36
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.36
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.36
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.36
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.36
1998 Barrett CW, Dill DL, Levitt JR. Decision procedure for bit-vector arithmetic Proceedings - Design Automation Conference. 522-527.  0.36
1996 Su JX, Dill DL, Barrett CW. Automatic generation of invariants in processor verification Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1166: 377-388. DOI: 10.1007/BFb0031822  0.36
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.36
1995 Barrett CW, Frost RL. Lattice-based designs of direct sum codebooks for vector quantization Data Compression Conference Proceedings. 436.  0.36
Show low-probability matches.