Publications

Papers about the tool

• Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. Lecture Notes in Computer Science, 2011, Volume 6806, Computer Aided Verification, pages 171-177.

Papers describing original research that was incorporated into CVC4

• Theory Combination
  • Dejan Jovanović and Clark Barrett. Sharing is Caring. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT '10), July 2010.
  • Dejan Jovanović and Clark Barrett. Polite Theories Revisited. In Proceedings of the Seventeenth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10), volume 6397 of Lecture Notes in Computer Science, pages 402-416. Springer, October 2010. Yogyakarta, Indonesia.
  • Dejan Jovanović and Clark Barrett. Being careful about theory combination. In Formal Methods in System Design, vol. 42, no. 1, Feb. 2013, pp. 67-90, Springer US.
• Bitvectors
  • Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, and Kshitij Bansal. A tale of two solvers: Eager and lazy approaches to bit-vectors. In Proceedings of the Twenty-Sixth International Conference on Computer Aided Verification (CAV '14), July 2014, pages 646-662. Vienna, Austria.
• Arithmetic
  • Tim King, Clark Barrett, and Bruno Dutertre. Simplex with sum of infeasibilities for SMT. In Formal Methods in Computer-Aided Design (FMCAD), 2013.
  • Tim King, Clark Barrett, and Cesare Tinelli. Leveraging linear and mixed integer programming for SMT. In FMCAD, 2014.
• Strings
  • Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. In Computer Aided Verification (CAV), 2014.
• Quantifiers and finite model finding
  • Andrew Reynolds, Cesare Tinelli, and Leonardo de Moura. Finding conflicting instances of quantified formulas in SMT. In FMCAD, 2014.
  • Andrew Reynolds, Cesare Tinelli, Amit Goel, and Sava Krstić. Finite model finding in SMT. In Computer Aided Verification (CAV), 2013.
  • Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstić, Morgan Deters, and Clark Barrett. Quantifier instantiation techniques for finite model finding in SMT. In CADE, 2013.

Applications of CVC4

• Tim King and Clark Barrett. Exploring and Categorizing Error Spaces using BMC and SMT. In Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT '11), July 2011.
• Wei Wang, Clark Barrett, and Thomas Wies. Cascade 2.0. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2014.