[Bib]
[PDF]
Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli.
Satisfiability Modulo Theories,
volume 185 of Frontiers in Artificial Intelligence and Applications,
chapter 26, pages 825-885. IOS Press, February 2009.
Web site.
[Abs]
[Bib]
[PS]
Yeting Ge, Clark Barrett, and Cesare Tinelli.
Solving Quantified Verification Conditions Using Satisfiability
Modulo Theories.
Annals of Mathematics and Artificial Intelligence, 55(1-2):101-122, February 2009.
[Abs]
[Bib]
[PS]
Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump.
Design and Results of the Third Satisfiability Modulo Theories Competition (SMT-COMP 2007).
International Journal on Artificial Intelligence Tools (IJAIT), 17(4):569-606, August 2008.
[Abs]
[Bib]
[PS]
Clark Barrett, Leonardo de Moura, and Aaron Stump.
Design and Results of the Second Satisfiability Modulo Theories Competition (SMT-COMP 2006).
Formal Methods in System Design, 31(3):221-239, 2007.
[Abs]
[Bib]
[PS]
Clark Barrett, Igor Shikanian, and Cesare Tinelli.
An Abstract Decision Procedure for a Theory of Inductive Data Types.
Journal on Satisfiability, Boolean Modeling and Computation, 3:21-46, 2007.
[Abs]
[Bib]
[PS]
Clark Barrett, Leonardo de Moura, and Aaron Stump.
Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005).
Journal of Automated Reasoning, 35(4):373-390, November 2005.
[Abs]
[Bib]
[PS]
Lenore Zuck, Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, and
Ying Hu.
Translation and Run-Time Validation of Loop Transformations.
Formal Methods in System Design, 27(3): 335-360, November 2005.
[Abs]
[Bib]
[PDF]
Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Tom Melham, Mark D.
Aagaard, Clark Barrett, and Don Syme.
An Industrially Effective Environment for Formal Hardware Verification.
IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems, 24(9): 1381-1405, September 2005.
[Abs]
[Bib]
[PDF]
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli.
CVC4.
In Ganesh Gopalakrishnan and Shaz Qadeer, editors,
Proceedings of the Twenty-Third International Conference on Computer Aided Verification (CAV '11), volume 6806
of
Lecture Notes in Computer Science,
pages 171-177. Springer, July 2011.
Snowbird, Utah.
[Abs]
[Bib]
[PDF]
Dejan Jovanović and Clark Barrett.
Polite Theories Revisited.
In Christian G. Fermüller and Andrei Voronkov, editors,
Proceedings of the Seventeenth International Conference on Logic for
Programming, Artificial Intelligence, and Reasoning (LPAR '10), volume 6397
of
Lecture Notes in Computer Science,
pages 402-416. Springer, October 2010.
Yogyakarta, Indonesia.
[Abs]
[Bib]
[PDF]
Christopher L. Conway and Clark Barrett.
Verifying Low-Level Implementations of High-Level Datatypes.
In Tayssir Touili, Byron Cook, and Paul Jackson, editors,
Proceedings of the Twenty-Second International Conference on Computer Aided
Verification (CAV '10), volume 6174 of
Lecture Notes in Computer Science, pages 306-320.
Springer, July 2010.
Edinburgh, Scotland.
[Abs]
[Bib]
[PDF]
Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett.
Pointer Analysis, Conditional Soundness, and Proving the Absence of
Errors.
In Maria Alpuente and German Vidal, editors, Proceedings
of the Fifteenth International Static Analysis Symposium (SAS '08), volume
5079 of
Lecture Notes in Computer Science, pages 62-77.
Springer, July 2008.
Valencia, Spain.
[Abs]
[Bib]
[PS]
Yeting Ge, Clark Barrett, and Cesare Tinelli.
Solving Quantified Verification Conditions using Satisfiability Modulo Theories.
In Frank Pfenning, editor, Proceedings of the
21st International Conference on Automated Deduction (CADE '07),
volume 4603 of
Lecture Notes in Artificial Intelligence, pages 167-182.
Springer-Verlag, July 2007.
Bremen, Germany.
[Abs]
[Bib]
[PS]
Clark Barrett and Cesare Tinelli.
CVC3.
In Werner Damm and Holger Hermanns, editors, Proceedings of the
19th International Conference on Computer Aided Verification (CAV '07),
volume 4590 of
Lecture Notes in Computer Science, pages 298-302.
Springer-Verlag, July 2007.
Berlin, Germany.
[Abs]
[Bib]
[PS]
Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.
Splitting on Demand in SAT Modulo Theories.
In Miki Hermann and Andrei Voronkov, editors, Proceedings of the
13th International Conference on Logic for Programming, Artificial
Intelligence, and Reasoning (LPAR '06),
volume 4246 of
Lecture Notes in Computer Science, pages 512-526. Springer-Verlag,
November 2006.
Phnom Penh, Cambodia.
[Abs]
[Bib]
[PS]
Nikhil Sethi and Clark Barrett.
CASCADE: C Assertion Checker and Deductive Engine.
In Thomas Ball and Robert B. Jones, editors, Proceedings of the
18th International Conference on Computer Aided Verification (CAV '06),
volume 4144 of
Lecture Notes in Computer Science, pages 166-169.
Springer-Verlag, August 2006.
Seattle, Washington.
[Abs]
[Bib]
[PS]
Clark Barrett, Leonardo de Moura, and Aaron Stump.
SMT-COMP: Satisfiability Modulo Theories Competition.
In Kousha Etessami and Sriram K. Rajamani, editors, Proceedings
of the 17th International Conference on Computer Aided Verification (CAV
'05), volume 3576 of
Lecture Notes in Computer Science, pages
20-23. Springer-Verlag, July 2005.
Edinburgh, Scotland.
[Abs]
[Bib]
[PS]
Clark Barrett, Yi Fang, Ben Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck.
TVOC: A Translation Validator for Optimizing Compilers.
In Kousha Etessami and Sriram K. Rajamani, editors, Proceedings
of the 17th International Conference on Computer Aided Verification (CAV
'05), volume 3576 of
Lecture Notes in Computer Science, pages
291-295. Springer-Verlag, July 2005.
Edinburgh, Scotland.
[Abs]
[Bib]
[PS]
Ying Hu, Clark Barrett, and Benjamin Goldberg.
Theory and Algorithms for the Generation and Validation of
Speculative Loop Optimizations.
In Proceedings of the Second IEEE International Conference on
Software Engineering and Formal Methods (SEFM '04), pages 281-289.
IEEE Computer Society, September 2004. Beijing, China.
[Abs]
[Bib]
[PS]
Clark Barrett and Sergey Berezin.
CVC Lite: A New Implementation of the Cooperating Validity Checker.
In Rajeev Alur and Doron A. Peled, editors, Proceedings of the
16th International Conference on Computer Aided Verification (CAV '04),
volume 3114 of
Lecture Notes in Computer Science, pages 515-518. Springer-Verlag, July 2004.
Boston, Massachusetts.
[Abs]
[Bib]
[PS]
Aaron Stump, Clark W. Barrett, and David L. Dill.
CVC: A Cooperating Validity Checker.
In Ed Brinksma and Kim Guldstrand Larsen, editors, Proceedings of the 14th International
Conference on Computer Aided Verification (CAV '02), volume 2404 of
Lecture Notes in Computer Science, pages 500-504. Springer-Verlag, 2002.
Copenhagen, Denmark.
[Abs]
[Bib]
[PS]
Clark W. Barrett, David L. Dill, and Aaron Stump.
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.
In Ed Brinksma and Kim Guldstrand Larsen, editors, Proceedings of the 14th International
Conference on Computer Aided Verification (CAV '02), volume 2404 of
Lecture Notes in Computer Science, pages 236-249. Springer-Verlag, 2002.
Copenhagen, Denmark.
[Abs]
[Bib]
[PS]
Aaron Stump, David L. Dill, Clark W. Barrett and Jeremy Levitt.
A Decision Procedure for an Extensional Theory of Arrays.
In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS '01),
pages 29-37. IEEE Computer Society, June 2001. Boston, Massachusetts.
[Abs]
[Bib]
[PS]
Clark W. Barrett, David L. Dill and Aaron Stump.
A Framework for Cooperating Decision Procedures.
In David McAllester, editor,
Proceedings of the 17th International Conference on Computer-Aided Deduction (CADE '00),
volume 1831 of
Lecture Notes in Artificial Intelligence, pages 79-97.
Springer-Verlag, June 2000. Pittsburgh, Pennsylvania.
[Abs]
[Bib]
[PS]
Clark W. Barrett, David L. Dill and Jeremy R. Levitt.
A Decision Procedure for Bit-Vector Arithmetic.
In Proceedings of the 35th
Design Automation Conference (DAC '98), pages 522-527, June 1998. San Francisco,
California. Best paper award.
[Abs]
[Bib]
[PS]
Jeffrey X. Su, David L. Dill and Clark W. Barrett.
Automatic Generation of Invariants in Processor Verification.
In Mandayam Srivas and Albert Camilleri, editors, Proceedings of
the First International Conference on Formal Methods
In Computer-Aided Design (FMCAD '96), volume 1166 of
Lecture Notes in Computer Science, pages 377-388. Springer-Verlag, November 1996.
Palo Alto, California.
[Abs]
[Bib]
[PS]
Clark W. Barrett, David L. Dill and Jeremy R. Levitt.
Validity Checking for Combinations of Theories with Equality.
In Mandayam Srivas and Albert Camilleri, editors, Proceedings of
the First International Conference on Formal Methods
In Computer-Aided Design (FMCAD '96), volume 1166 of
Lecture Notes in Computer Science, pages 187-201. Springer-Verlag, November 1996.
Palo Alto, California.
[Abs]
[Bib]
[PDF]
Tim King and Clark Barrett.
Exploring and Categorizing Error Spaces using BMC and SMT.
In Shuvendu Lahhiri and Sanjit Seshia, editors, Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT '11), July 2011.
Snowbird, Utah.
[Abs]
[Bib]
[PDF]
Clark Barrett, Aaron Stump, and Cesare Tinelli.
The SMT-LIB standard -- version 2.0.
In Aarti Gupta and Daniel Kroening, editors, Proceedings of the 8th International Workshop
on Satisfiability Modulo Theories (SMT '10), July 2010.
Edinburgh, Scotland, United Kingdom.
[Abs]
[Bib]
[PDF]
Dejan Jovanović and Clark Barrett.
Sharing is Caring.
In Aarti Gupta and Daniel Kroening, editors, Proceedings of the 8th International Workshop
on Satisfiability Modulo Theories (SMT '10), July 2010.
Edinburgh, Scotland, United Kingdom.
[Abs]
[Bib]
[PDF]
Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump, and Clark Barrett.
Comparing Proof Systems for Linear Real Arithmetic with LFSC.
In Aarti Gupta and Daniel Kroening, editors, Proceedings of the 8th International Workshop
on Satisfiability Modulo Theories (SMT '10), July 2010.
Edinburgh, Scotland, United Kingdom.
[Abs]
[Bib]
[PS]
Clark Barrett, Igor Shikanian, and Cesare Tinelli.
An Abstract Decision Procedure for Satisfiability in the Theory of
Recursive Data Types.
In Byron Cook and Roberto Sebastiani, editors, Combined Proceedings of the 4th Workshop
on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '06) and the 1st International
Workshop on Probabilistic Automata and Logics (PaUL '06), volume 174(8) of
Electronic Notes in Theoretical Computer Science, pages 23-37. Elsevier, June 2007.
Seattle, Washington.
[Abs]
[Bib]
[PS]
Sean McLaughlin, Clark Barrett, and Yeting Ge.
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite.
In Alessandro Armando and Alessandro Cimatti, editors,
Proceedings of the Third Workshop on Pragmatics of Decision Procedures in
Automated Reasoning (PDPAR '05), volume 144(2) of Electronic Notes in
Theoretical Computer Science, pages 43-51. Elsevier, January 2006.
Edinburgh, Scotland.
[Abs]
[Bib]
[PS]
Ying Hu, Clark Barrett, Benjamin Goldberg, and Amir Pnueli.
Validating more Loop Optimizations.
In J. Knoop, G.C. Necula, and W. Zimmermann, editors,
Proceedings of the Fourth International Workshop on Compiler Optimization
meets Compiler Verificaiton (COCV '05), volume 141(2) of Electronic
Notes in Theoretical Computer Science, pages 69-84. Elsevier, December
2005.
Edinburgh, Scotland.
[Abs]
[Bib]
[PS]
Benjamin Goldberg, Lenore Zuck, and Clark Barrett.
Into the Loops: Practical Issues in Translation Validation for Optimizing
Compilers.
In J. Knoop, G.C. Necula, and W. Zimmermann, editors,
Proceedings of the Third International Workshop on Compiler Optimization
meets Compiler Verificaiton (COCV '04), volume 132(1) of Electronic
Notes in Theoretical Computer Science, pages 53-71. Elsevier, May 2005. Barcelona, Spain.
[Abs]
[Bib]
[PS]
Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel,
and David L. Dill.
A Practical Approach to Partial Functions in CVC Lite.
In Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio
Ranise, and Cesare Tinelli, editors, Selected Papers from the Workshops
on Disproving and the Second International Workshop on Pragmatics of Decision
Procedures (PDPAR '04), volume 125(3) of Electronic Notes in
Theoretical Computer Science, pages 13-23. Elsevier, July 2005. Cork, Ireland.
[Abs]
[Bib]
[PS]
Clark Barrett and Jacob Donham.
Combining SAT Methods with Non-Clausal Decision Heuristics.
In Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio
Ranise, and Cesare Tinelli, editors, Selected Papers from the Workshops
on Disproving and the Second International Workshop on Pragmatics of Decision
Procedures (PDPAR '04), volume 125(3) of Electronic Notes in
Theoretical Computer Science, pages 3-12. Elsevier, July 2005. Cork, Ireland.
[Abs]
[Bib]
[PS]
Clark Barrett and Sergey Berezin.
A Proof-Producing Boolean Search Engine.
In Proceedings of the First International Workshop on
Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03), July,
2003. Miami, Florida.
[Abs]
[Bib]
[PS]
Clark Barrett, Benjamin Goldberg, and Lenore Zuck.
Run-Time Validation of Speculative Optimizations using CVC.
In Oleg Sokolsky and Mahesh Viswanathan, editors, Proceedings of the Third International
Workshop on Run-time Verification (RV '03), volume 89(2) of Electronic
Notes in Theoretical Computer Science, pages 89-107. Elsevier, October 2003. Boulder, Colorado.
[Abs]
[Bib]
[PS]
Clark W. Barrett, David L. Dill, and Aaron Stump.
A Generalization of Shostak's Method for Combining Decision Procedures.
In Alessandro Armando, editor, Proceedings of the Fourth
International Workshop on Frontiers of Combining Systems (FroCoS '02),
volume 2309 of
Lecture Notes in Artificial Intelligence, pages
132-146. Springer-Verlag, April 2002.
Santa Margherita Ligure, Italy.
[Abs]
[Bib]
[PS]
Aaron Stump, Clark W. Barrett, and David L. Dill.
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF.
In Frank Pfenning, editor, Proceedings of the Third International
Workshop on Logical Frameworks and Meta-Languages (LFM '02), volume 70(2) of Electronic
Notes in Theoretical Computer Science, pages 29-41. Elsevier, July 2002. Copehnagen, Denmark.
[Abs]
[Bib]
[PDF]
Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump.
Design and Results of the Fourth Annual Satisfiability Modulo
Theories Competition (SMT-COMP 2008).
Technical Report TR2010-931, Depatrment of Computer Science,
New York University, July 2010.
[Abs]
[Bib]
[PDF]
Dejan Jovanović and Clark Barrett.
Polite Theories Revisited.
Technical Report TR2010-922, Depatrment of Computer Science,
New York University, January 2010.
[Abs]
[Bib]
[PDF]
Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett.
Points-to Analysis, Conditional Soundness, and Proving the Absence of
Errors.
Technical Report TR2008-910, Depatrment of Computer Science,
New York University, March 2008.
[Abs]
[Bib]
[PDF]
Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.
Splitting on demand in SAT Modulo Theories.
Technical Report 06-05, Department of Computer Science,
University of Iowa, August 2006.
[Abs]
[Bib]
[PS]
Clark Barrett, Igor Shikanian, and Cesare Tinelli.
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive
Data Types. Technical Report TR2005-878, Department of Computer Science,
New York University, November 2005.
[Abs]
[Bib]
[PS]
[PPT]
Clark W. Barrett. Checking Validity of Quantifier-Free Formulas in
Combinations of First-Order Theories. PhD Thesis, Stanford University, 2003.
Stanford, California.
[Link]
Jeremy R. Levitt, Christophe G. Gauthron, Clark W. Barrett, Lawrence Curtis Widdoes Jr. Reuse of Learned Information to Simplify Functional Verification of a Digital Circuit, December 2007, Patent #20070299648.