Publications

If you are citing CVC4, please use the following BibTex entry:

@inproceedings{DBLP:conf/cav/BarrettCDHJKRT11,
  author    = {Clark W. Barrett and
               Christopher L. Conway and
               Morgan Deters and
               Liana Hadarean and
               Dejan Jovanovic and
               Tim King and
               Andrew Reynolds and
               Cesare Tinelli},
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  title     = {{CVC4}},
  booktitle = {Computer Aided Verification - 23rd International Conference, {CAV}
               2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6806},
  pages     = {171--177},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-22110-1\_14},
  doi       = {10.1007/978-3-642-22110-1\_14},
  biburl    = {https://dblp.org/rec/conf/cav/BarrettCDHJKRT11.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

To Appear

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli. Towards Satisfiability Modulo Parametric Bit-Vectors. In Journal of Automated Reasoning, to appear.
PDF Artifact

2021

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. Syntax-Guided Quantifier Instantiation. In Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21), 2021. Nominated for the EATCS Best ETAPS Theory Paper Award.
PDF DOI Bibtex Artifact

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli. On Solving Quantified Bit-Vector Constraints using Invertibility Conditions. In Formal Methods in Computer-Aided Design (FMSD), 2021.
PDF DOI Artifact

2020

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett. Politeness for the Theory of Algebraic Datatypes. In International Joint Conference on Automated Reasoning (IJCAR), 2020. Best Paper.
PDF DOI Bibtex

Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli. Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. In International Joint Conference on Automated Reasoning (IJCAR), 2020.
PDF DOI Bibtex

Clark Barrett, Haniel Barbosa, Martin Brain, Ahmed Irfan, Makai Mann, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Amalee Wilson, Yoni Zohar. CVC4 at the SMT Competition 2020. In Technical Report, 2020.
PDF Bibtex

Andrew Reynolds, Andres Nötzli, Clark Barrett, Cesare Tinelli. Reductions for Strings and Regular Expressions Revisited. In Formal Methods in Computer-Aided Design (FMCAD), 2020.
PDF

Andrew Reynolds, Andres Nötzli, Clark Barrett, Cesare Tinelli. A Decision Procedure for String to Code Point Conversion. In International Joint Conference on Automated Reasoning (IJCAR), 2020.
PDF Bibtex Artifact

2019

Clark Barrett, Haniel Barbosa, Martin Brain, Tim King, Makai Mann, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar. CVC4 at the SMT competition 2019. In Proceedings of the 17th International Workshop on Satisfiability Modulo Theories (SMT’19), 2019.
PDF Bibtex

Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli. Extending enumerative function synthesis via SMT-driven classification. In Formal Methods in Computer-Aided Design (FMCAD), 2019. Best Paper Honorable Mention.
PDF DOI Bibtex

Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, Morgan Deters. Refutation-based synthesis in SMT. In Formal Methods in System Design, 2019.
PDF DOI Bibtex

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli. Towards bit-width-independent proofs in SMT solvers. In Proceedings of the 27th International Conference on Automated Deduction (CADE’19), 2019.
PDF DOI Bibtex Artifact

Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark Barrett. Extending SMT solvers to higher-order logic. In Proceedings of the 27th International Conference on Automated Deduction (CADE’19), 2019.
PDF DOI Bibtex

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, Cesare Tinelli. Syntax-guided rewrite rule enumeration for SMT solvers. In Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT’19), 2019.
PDF DOI Bibtex

Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark Barrett. DRAT-based bit-vector proofs in CVC4. In Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT’19), 2019.
PDF DOI Bibtex

Andrew Reynolds, Andres Nötzli, Clark Barrett, Cesare Tinelli. High-level abstractions for simplifying extended string constraints in SMT. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV’19), 2019.
PDF DOI Bibtex

Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Cesare Tinelli, Clark Barrett. CVC4SY: Smart and fast term enumeration for syntax-guided synthesis. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV’19), 2019.
PDF DOI Bibtex

Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. Invertibility conditions for floating-point formulas. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV’19), 2019.
PDF DOI Bibtex Artifact

2018

Andrew Reynolds, Haniel Barbosa, Pascal Fontaine. Revisiting Enumerative Instantiation. In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), 2018.
PDF DOI Bibtex

Clark Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli. CVC4 at the SMT Competition 2018. In CoRR abs/1806.08775, 2018.
PDF Bibtex Arxiv

Kshitij Bansal, Clark Barrett, Andrew Reynolds, Cesare Tinelli. Reasoning with finite sets and cardinality constraints in SMT. In Logical Methods in Computer Science, 2018.
PDF DOI Bibtex

Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark Barrett. Datatypes with shared selectors. In Proceedings of the 9th international joint conference on Automated Reasoning (IJCAR’18), 2018.
PDF DOI Bibtex Artifact

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. Solving quantified bit-vectors using invertibility conditions. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV’18), 2018.
PDF DOI Bibtex Artifact

2017

Andrew Reynolds, Cesare Tinelli. SyGuS Techniques in the Core of an SMT solver. In Proceedings of the 6th Workshop on Synthesis (SYNT@CAV’17), 2017.
PDF DOI Bibtex

Haniel Barbosa, Pascal Fontaine, Andrew Reynolds. Congruence Closure with Free Variables. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17), 2017.
PDF DOI Bibtex

Andrew Reynolds, Radu Iosif, Christina Serban. Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. In Proceedings of the 18th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’17), 2017.
PDF DOI Bibtex

Andrew Reynolds, Tim King, Viktor Kuncak. Solving quantified linear arithmetic by counterexample-guided instantiation. In Formal Methods in System Design, 2017.
PDF DOI Bibtex

Andrew Reynolds, Cesare Tinelli, Clark Barrett. Constraint solving for finite model finding in SMT solvers. In TPLP, 2017.
PDF DOI Bibtex

Andrew Reynolds, Jasmin Christian Blanchette. A decision procedure for (co)datatypes in SMT solvers. In J. Autom. Reasoning, 2017.
PDF DOI Bibtex

Andrew Reynolds, Cesare Tinelli, Dejan Jovanović, Clark Barrett. Designing theory solvers with extensions. In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FROCOS’17), 2017.
PDF DOI Bibtex Artifact

Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark Barrett. Relational constraint solving in SMT. In Proceedings of the 26th International Conference on Automated Deduction (CADE’17), 2017.
PDF DOI Bibtex Artifact

Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark Barrett. SMTCoq: A plug-in for integrating SMT solvers into Coq. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV’17), 2017.
PDF DOI Bibtex

Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli. Scaling up DPLL(T) string solvers using context-dependent simplification. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV’17), 2017.
PDF DOI Bibtex Artifact

2016

Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli. Model Finding for Recursive Functions in SMT. In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR’16), 2016.
PDF DOI Bibtex

Andrew Reynolds, Radu Iosif, Christina Serban, Tim King. A Decision Procedure for Separation Logic in SMT. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16), 2016.
PDF DOI Bibtex

Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, Morgan Deters. An efficient SMT solver for string constraints. In Formal Methods in System Design, 2016.
PDF DOI Bibtex

Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean. Lazy proofs for DPLL(T)-based SMT solvers. In Proceedings of the 16th International Conference on Formal Methods in Computer-Aided design (FMCAD’16), 2016. Best Paper.
PDF DOI Bibtex

Kshitij Bansal, Andrew Reynolds, Clark Barrett, Cesare Tinelli. A new decision procedure for finite sets and cardinality constraints in SMT. In Proceedings of the 8th international joint conference on Automated Reasoning (IJCAR’16), 2016.
PDF DOI Bibtex

2015

Andrew Reynolds, Viktor Kuncak. Induction for SMT solvers. In Proceedings of the 16th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’15), 2015.
PDF DOI Bibtex

Andrew Reynolds, Jasmin Christian Blanchette. A Decision Procedure for (Co)datatypes in SMT solver. In Proceedings of the 25th International Conference on Automated Deduction (CADE’15), 2015.
PDF DOI Bibtex

Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters. Fine-grained SMT proofs for the theory of fixed-width bit-vectors. In Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’15), 2015.
PDF DOI Bibtex

Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark Barrett. A decision procedure for regular membership and length constraints over unbounded strings. In Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FROCOS’15), 2015.
PDF DOI Bibtex

Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark Barrett, Cesare Tinelli. Counterexample guided quantifier instantiation for synthesis in SMT. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV’15), 2015.
PDF DOI Bibtex

Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, Thomas Wies. Deciding local theory extensions via E-matching. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV’15), 2015.
PDF DOI Bibtex

2014

Andrew Reynolds, Cesare Tinelli, Leonardo Mendonca de Moura. Finding conflicting instances of quantified formulas in SMT. In Formal Methods in Computer-Aided Design (FMCAD’14), 2014.
PDF DOI Bibtex

Tim King, Clark Barrett, Cesare Tinelli. Leveraging linear and mixed integer programming for SMT. In Proceedings of the 14th International Conference on Formal Methods in Computer-Aided design (FMCAD’14), 2014.
PDF DOI Bibtex

Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, Kshitij Bansal. A tale of two solvers: Eager and lazy approaches to bit-vectors. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV’14), 2014.
PDF DOI Bibtex

Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV’14), 2014.
PDF DOI Bibtex Artifact

2013

Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic. Finite Model Finding in SMT. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13), 2013.
PDF DOI Bibtex

Dejan Jovanovic, Clark Barrett. Being careful about theory combination. In Formal Methods in System Design, 2013.
PDF DOI Bibtex

Timothy King, Clark Barrett, Bruno Dutertre. Simplex with sum of infeasibilities for SMT. In Proceedings of the 13th International Conference on Formal Methods in Computer-Aided design (FMCAD’13), 2013.
PDF Bibtex

Dejan Jovanović, Clark Barrett, Leonardo Moura. The design and implementation of the model constructing satisfiability calculus. In Proceedings of the 13th International Conference on Formal Methods in Computer-Aided design (FMCAD’13), 2013.
PDF

Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark Barrett. Quantifier instantiation techniques for finite model finding in SMT. In Proceedings of the 24th International Conference on Automated Deduction (CADE’13), 2013.
PDF DOI Bibtex Artifact

2011

Dejan Jovanović, Clark Barrett. Sharing is caring: Combination of theories. In Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FROCOS’11), 2011.
PDF DOI Bibtex

Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, Cesare Tinelli. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11), 2011.
PDF DOI Bibtex

2010

Dejan Jovanović, Clark Barrett. Polite Theories Revisited. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’10), 2010.
PDF DOI Bibtex