Also see publications by category

**“Proofs in Satisfiability Modulo Theories”**

by Clark Barrett, Leonardo de Moura, and Pascal Fontaine.

In *All about Proofs, Proofs for All*, of Mathematical Logic and Foundations, (David Delahaye and Bruno Woltzenlogel Paleo, eds.), (London, UK), Jan. 2015.

Details.

**“Satisfiability Modulo Theories”**

by Clark Barrett and Cesare Tinelli.

In *Handbook of Model Checking*, (Ed Clarke, Thomas Henzinger, and Helmut Veith, eds.), 2014. In preparation.

Details.

**“Leveraging Linear and Mixed Integer Programming for SMT”**

by Tim King, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 14^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '14)*, Oct. 2014, pp. 139-146. Lausanne, Switzerland.

Details.

**“A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions”**

by Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters.

In *Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14)*, (Armin Biere and Roderick Bloem, eds.), July 2014, pp. 646-662. Vienna, Austria.

Details.

**“A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors”**

by Liana Hadarean, Clark Barrett, Dejan Jovanovic, Cesare Tinelli, and Kshitij Bansal.

In *Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14)*, (Armin Biere and Roderick Bloem, eds.), July 2014, pp. 680-695. Vienna, Austria.

Details.

**“Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories”**

by Clark Barrett, Daniel Kroening, and Thomas Melham.

London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering technical report 3, June 2014. Knowledge Transfer Report.

Details.

**“Cascade 2.0”**

by Wei Wang, Clark Barrett, and Thomas Wies.

In *Proceedings of the 15^th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '14)*, (Kenneth L. McMillan and Xavier Rival, eds.), Jan. 2014, pp. 142-160. San Diego, California.

Details.

**“Quantifier Instantiation Techniques for Finite Model Finding in SMT”**

by Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, and Clark Barrett.

In *Proceedings of the 24^th International Conference on Automated Deduction (CADE '13)*, (Maria Paola Bonacina, ed.), 2013, pp. 377-391. Lake Placid, NY.

Details.

**““Decision Procedures:An Algorithmic Point of View,”**

by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008” by Clark Barrett.

*Journal of Automated Reasoning*, vol. 51, no. 4, Dec. 2013, pp. 453-456, Springer Netherlands.

Details.

**“The Design and Implementation of the Model Constructing Satisfiability Calculus”**

by Dejan Jovanovic, Clark Barrett, and Leonardo de Moura.

In *Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13)*, Oct. 2013. Portland, Oregon.

Details.

**“Simplex with Sum of Infeasibilities for SMT”**

by Timothy King, Clark Barrett, and Bruno Dutertre.

In *Proceedings of the 13^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13)*, Oct. 2013, pp. 189-196. Portland, Oregon.

Details.

**“Witness Runs for Counter Machines”**

by Clark Barrett, Stephané Demri, and Morgan Deters.

In *Proceedings of the 9^th International Symposium on Frontiers of Combining Systems (FroCoS '13)*, (Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, eds.), Sep. 2013, pp. 120-150. Nancy, France.

Details.

**“6 Years of SMT-COMP”**

by Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras, and Aaron Stump.

*Journal of Automated Reasoning*, vol. 50, no. 3, Mar. 2013, pp. 243-277, Springer Netherlands.

Details.

**“Being Careful about Theory Combination”**

by Dejan Jovanovic and Clark Barrett.

*Formal Methods in System Design*, vol. 42, no. 1, Feb. 2013, pp. 67-90, Springer US.

Details.

**“Sharing is Caring: Combination of Theories”**

by Dejan Jovanovic and Clark Barrett.

In *Proceedings of the 8^th International Symposium on Frontiers of Combining Systems (FroCoS '11)*, (Cesare Tinelli and Viorica Sofronie-Stokkermans, eds.), Oct. 2011, pp. 195-210. Saarbrücken, Germany.

Details.

**“Sharing is Caring: Combination of Theories”**

by Dejan Jovanovic and Clark Barrett, Depatrment of Computer Science.

New York University technical report TR2011-940, Oct. 2011.

Details.

**“CVC4”**

by Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli.

In *Proceedings of the 23^rd International Conference on Computer Aided Verification (CAV '11)*, (Ganesh Gopalakrishnan and Shaz Qadeer, eds.), July 2011, pp. 171-177. Snowbird, Utah.

Details.

**“Exploring and Categorizing Error Spaces using BMC and SMT”**

by Tim King and Clark Barrett.

In *Proceedings of the 9^th International Workshop on Satisfiability Modulo Theories (SMT '11)*, July 2011. Snowbird, Utah.

Details.

**“Polite Theories Revisited”**

by Dejan Jovanovic and Clark Barrett.

In *Proceedings of the 17^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10)*, (Christian G. Fermüller and Andrei Voronkov, eds.), Oct. 2010, pp. 402-416. Yogyakarta, Indonesia.

Details.

**“Verifying Low-Level Implementations of High-Level Datatypes”**

by Christopher L. Conway and Clark Barrett.

In *Proceedings of the 22^nd International Conference on Computer Aided Verification (CAV '10)*, (Tayssir Touili, Byron Cook, and Paul Jackson, eds.), July 2010, pp. 306-320. Edinburgh, Scotland.

Details.

**“The SMT-LIB Standard -- Version 2.0”**

by Clark Barrett, Aaron Stump, and Cesare Tinelli.

In *Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10)*, July 2010. Edinburgh, Scotland.

Details.

**“Sharing is Caring”**

by Dejan Jovanovic and Clark Barrett.

In *Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10)*, July 2010. Edinburgh, Scotland.

Details.

**“Design and Results of the 4^th Annual Satisfiability Modulo Theories Competition (SMT-COMP 2008)”**

by Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump, Depatrment of Computer Science.

New York University technical report TR2010-931, July 2010.

Details.

**“Comparing Proof Systems for Linear Real Arithmetic with LFSC”**

by Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump, and Clark Barrett.

In *Proceedings of the 8^th International Workshop on Satisfiability Modulo Theories (SMT '10)*, July 2010. Edinburgh, Scotland.

Details.

**“Polite Theories Revisited”**

by Dejan Jovanovic and Clark Barrett, Depatrment of Computer Science.

New York University technical report TR2010-922, Jan. 2010.

Details.

**“Solving Quantified Verification Conditions using Satisfiability Modulo Theories”**

by Yeting Ge, Clark Barrett, and Cesare Tinelli.

*Annals of Mathematics and Artificial Intelligence*, vol. 55, no. 1-2, Feb. 2009, pp. 101-122, Springer.

Details.

**“Satisfiability Modulo Theories”**

by Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli.

In *Handbook of Satisfiability*, vol. 185 of Frontiers in Artificial Intelligence and Applications, (Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, eds.), Feb. 2009, pp. 825-885.

Details.

**“Design and Results of the 3^rd Annual Satisfiability Modulo Theories Competition (SMT-COMP 2007)”**

by Clark Barrett, Morgan Deters, Albert Oliveras, and Aaron Stump.

Details.

**“Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors”**

by Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett.

In *Proceedings of the 15^th International Static Analysis Symposium (SAS '08)*, (Mara Alpuente and Germán Vidal, eds.), July 2008, pp. 62-77. Valencia, Spain.

Details.

**“Points-to Analysis, Conditional Soundness, and Proving the Absence of Errors”**

by Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett, Depatrment of Computer Science.

New York University technical report TR2008-910, Mar. 2008.

Details.

**“An Abstract Decision Procedure for a Theory of Inductive Data Types”**

by Clark Barrett, Igor Shikanian, and Cesare Tinelli.

*Journal on Satisfiability, Boolean Modeling and Computation*, vol. 3, 2007, pp. 21-46, IOS Press.

Details.

**“Reuse of learned information to simplify functional verification of a digital circuit”**

by Jeremy R. Levitt, Christophe G. Gauthron, Clark W. Barrett, and Lawrence Curtis Widdoes Jr..

Dec. 2007. Patent No. 20070299648.

Details.

**“Design and Results of the 2^nd Satisfiability Modulo Theories Competition (SMT-COMP 2006)”**

by Clark Barrett, Leonardo de Moura, and Aaron Stump.

Details.

**“CVC3”**

by Clark Barrett and Cesare Tinelli.

In *Proceedings of the 19^th International Conference on Computer Aided Verification (CAV '07)*, (Werner Damm and Holger Hermanns, eds.), July 2007, pp. 298-302. Berlin, Germany.

Details.

**“Solving Quantified Verification Conditions using Satisfiability Modulo Theories”**

by Yeting Ge, Clark Barrett, and Cesare Tinelli.

In *Proceedings of the 21^st International Conference on Automated Deduction (CADE '07)*, (Frank Pfenning, ed.), July 2007, pp. 167-182. Bremen, Germany.

Details.

**“An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types”**

by Clark Barrett, Igor Shikanian, and Cesare Tinelli.

In *Combined Proceedings of the 4^th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '06) and the 1^st International Workshop on Probabilistic Automata and Logics (PaUL '06)*, (Byron Cook and Roberto Sebastiani, eds.), June 2007, pp. 23-37. Seattle, Washington.

Details.

**“Splitting on Demand in SAT Modulo Theories”**

by Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.

In *Proceedings of the 13^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '06)*, (Miki Hermann and Andrei Voronkov, eds.), Nov. 2006, pp. 512-526. Phnom Penh, Cambodia.

Details.

**“CASCADE: C Assertion Checker and Deductive Engine”**

by Nikhil Sethi and Clark Barrett.

In *Proceedings of the 18^th International Conference on Computer Aided Verification (CAV '06)*, (Thomas Ball and Robert B. Jones, eds.), Aug. 2006, pp. 166-169. Seattle, Washington.

Details.

**“Splitting on Demand in SAT Modulo Theories”**

by Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli, Department of Computer Science.

University of Iowa technical report 06-05, Aug. 2006.

Details.

**“Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite”**

by Sean McLaughlin, Clark Barrett, and Yeting Ge.

In *Proceedings of the 3^rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05)*, (Alessandro Armando and Alessandro Cimatti, eds.), Jan. 2006, pp. 43-51. Edinburgh, Scotland.

Details.

**“Validating More Loop Optimizations”**

by Ying Hu, Clark Barrett, Benjamin Goldberg, and Amir Pnueli.

In *Proceedings of the 4^th International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '05)*, (J. Knoop, G.C. Necula, and W. Zimmermann, eds.), Dec. 2005, pp. 69-84. Edinburgh, Scotland.

Details.

**“Translation and Run-Time Validation of Loop Transformations”**

by Lenore Zuck, Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, and Ying Hu.

*Formal Methods in System Design*, vol. 27, no. 3, Nov. 2005, pp. 335-360, Springer Netherlands.

Details.

**“Design and Results of the 1^st Satisfiability Modulo Theories Competition (SMT-COMP 2005)”**

by Clark Barrett, Leonardo de Moura, and Aaron Stump.

Details.

**“An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types”**

by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Department of Computer Science.

New York University technical report TR2005-878, Nov. 2005.

Details.

**“An Industrially Effective Environment for Formal Hardware Verification”**

by Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Tom Melham, Mark D. Aagaard, Clark Barrett, and Don Syme.

*IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*, vol. 24, no. 9, Sep. 2005, pp. 1381-1405.

Details.

**“TVOC: A Translation Validator for Optimizing Compilers”**

by Clark Barrett, Yi Fang, Ben Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck.

In *Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05)*, (Kousha Etessami and Sriram K. Rajamani, eds.), July 2005, pp. 291-295. Edinburgh, Scotland.

Details.

**“SMT-COMP: Satisfiability Modulo Theories Competition”**

by Clark Barrett, Leonardo de Moura, and Aaron Stump.

In *Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05)*, (Kousha Etessami and Sriram K. Rajamani, eds.), July 2005, pp. 20-23. Edinburgh, Scotland.

Details.

**“Combining SAT Methods with Non-Clausal Decision Heuristics”**

by Clark Barrett and Jacob Donham.

In *Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04)*, (Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, eds.), July 2005, pp. 3-12. Cork, Ireland.

Details.

**“A Practical Approach to Partial Functions in CVC Lite”**

by Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, and David L. Dill.

In *Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR '04)*, (Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, eds.), July 2005, pp. 13-23. Cork, Ireland.

Details.

**“Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers”**

by Benjamin Goldberg, Lenore Zuck, and Clark Barrett.

In *Proceedings of the 3^rd International Workshop on Compiler Optimization meets Compiler Verificaiton (COCV '04)*, (J. Knoop, G.C. Necula, and W. Zimmermann, eds.), May 2005, pp. 53-71. Barcelona, Spain.

Details.

**“Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations”**

by Ying Hu, Clark Barrett, and Benjamin Goldberg.

In *Proceedings of the 2^nd IEEE International Conference on Software Engineering and Formal Methods (SEFM '04)*, Sep. 2004, pp. 281-289. Beijing, China.

Details.

**“CVC Lite: A New Implementation of the Cooperating Validity Checker”**

by Clark Barrett and Sergey Berezin.

In *Proceedings of the 16^th International Conference on Computer Aided Verification (CAV '04)*, (Rajeev Alur and Doron A. Peled, eds.), July 2004, pp. 515-518. Boston, Massachusetts.

Details.

**“Run-Time Validation of Speculative Optimizations using CVC”**

by Clark Barrett, Benjamin Goldberg, and Lenore Zuck.

In *Proceedings of the 3^rd International Workshop on Run-time Verification (RV '03)*, (Oleg Sokolsky and Mahesh Viswanathan, eds.), Oct. 2003, pp. 89-107. Boulder, Colorado.

Details.

**“A Proof-Producing Boolean Search Engine”**

by Clark Barrett and Sergey Berezin.

In *Proceedings of the 1^st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03)*, July 2003. Miami, Florida.

Details.

**“Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories”**

by Clark W. Barrett.

Ph.D. dissertation, Stanford University, Jan. 2003. Stanford, California.

Details.

**“CVC: A Cooperating Validity Checker”**

by Aaron Stump, Clark W. Barrett, and David L. Dill.

In *Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02)*, (Ed Brinksma and Kim Guldstrand Larsen, eds.), July 2002, pp. 500-504. Copenhagen, Denmark.

Details.

**“Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF”**

by Aaron Stump, Clark W. Barrett, and David L. Dill.

In *Proceedings of the 3^rd International Workshop on Logical Frameworks and Meta-Languages (LFM '02)*, (Frank Pfenning, ed.), July 2002, pp. 29-41. Copenhagen, Denmark.

Details.

**“Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT”**

by Clark W. Barrett, David L. Dill, and Aaron Stump.

In *Proceedings of the 14^th International Conference on Computer Aided Verification (CAV '02)*, (Ed Brinksma and Kim Guldstrand Larsen, eds.), July 2002, pp. 236-249. Copenhagen, Denmark.

Details.

**“A Generalization of Shostak's Method for Combining Decision Procedures”**

by Clark W. Barrett, David L. Dill, and Aaron Stump.

In *Proceedings of the 4^th International Workshop on Frontiers of Combining Systems (FroCoS '02)*, (Alessandro Armando, ed.), Apr. 2002, pp. 132-146. Santa Margherita Ligure, Italy.

Details.

**“A Decision Procedure for an Extensional Theory of Arrays”**

by Aaron Stump, Clark W. Barrett, David L. Dill, and Jeremy Levitt.

In *Proceedings of the 16^th IEEE Symposium on Logic in Computer Science (LICS '01)*, June 2001, pp. 29-37. Boston, Massachusetts.

Details.

**“A Framework for Cooperating Decision Procedures”**

by Clark W. Barrett, David L. Dill, and Aaron Stump.

In *Proceedings of the 17^th International Conference on Computer-Aided Deduction (CADE '00)*, (David McAllester, ed.), June 2000, pp. 79-97. Pittsburgh, Pennsylvania.

Details.

**“A Decision Procedure for Bit-vector Arithmetic”**

by Clark W. Barrett, David L. Dill, and Jeremy R. Levitt.

In *Proceedings of the 35^th Design Automation Conference (DAC '98)*, June 1998, pp. 522-527. San Francisco, California.

Details.

**“Validity Checking for Combinations of Theories with Equality”**

by Clark W. Barrett, David L. Dill, and Jeremy R. Levitt.

In *Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96)*, (Mandayam Srivas and Albert Camilleri, eds.), Nov. 1996, pp. 187-201. Palo Alto, California.

Details.

**“Automatic Generation of Invariants in Processor Verification”**

by Jeffrey X. Su, David L. Dill, and Clark W. Barrett.

In *Proceedings of the 1^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96)*, (Mandayam Srivas and Albert Camilleri, eds.), Nov. 1996, pp. 377-388. Palo Alto, California.

Details.

(This webpage was created with bibtex2web.)