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

About

News

Downloads

Documentation

Publications

Awards

People

History

Third-Party Applications

Acknowledgements

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"
}
```

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]

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]

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]

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]

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]

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]

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]

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]

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]