CVC4

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

About
News
Downloads
Publications
People
History
Third-Party Applications
Acknowledgements

Try CVC4 online!


Publications

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

@inproceedings{BCD+11,
  url       = "<a href="http://www.cs.stanford.edu/~barrett/pubs/BCD+11.pdf">http://www.cs.stanford.edu/~barrett/pubs/BCD+11.pdf</a>",
  author    = "Clark Barrett and Christopher L. Conway and Morgan Deters and
               Liana Hadarean and Dejan Jovanovi{'{c}} and Tim King and
               Andrew Reynolds and Cesare Tinelli",
  title     = "{CVC4}",
  booktitle = "Proceedings of the 23rd International Conference on Computer Aided Verification (CAV '11)",
  series    = "Lecture Notes in Computer Science",
  volume    = 6806,
  publisher = "Springer",
  editor    = "Ganesh Gopalakrishnan and Shaz Qadeer",
  pages     = "171--177",
  month     = jul,
  year      = 2011,
  note      = "Snowbird, Utah",
  category  = "Conference Publications"
}

2019

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]

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]

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]

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]

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]

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]

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]

2018

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]

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]

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]

2017

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

Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, Morgan Deters. Refutation-based synthesis in smt. In Formal Methods in System Design, 2017.
[PDF]

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

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

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]

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]

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]

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]

2016

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]

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.
[PDF]

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]

2015

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]

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]

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]

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]

2014

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]

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]

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]

2013

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

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]

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]

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]

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]

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]