Clark Barrett's Publications

Also see publications by category


2015

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.

2014

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.

2013

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.

2011

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.

2010

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.

2009

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.

2008

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.
International Journal on Artificial Intelligence Tools (IJAIT), vol. 17, no. 4, Aug. 2008, pp. 569-606, World Scientific.
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.

2007

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.
Formal Methods in System Design, vol. 31, no. 3, Dec. 2007, pp. 221-239, Springer Netherlands.
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.

2006

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.

2005

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.
Journal of Automated Reasoning, vol. 35, no. 4, Nov. 2005, pp. 373-390, Springer Netherlands.
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.

2004

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.

2003

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.

2002

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.

2001

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.

2000

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.

1998

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. Best paper award.
Details.

1996

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.)