CVC4

by Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, Cesare Tinelli
Abstract:
CVC4 is the latest version of the Cooperating Validity Checker. A joint project of NYU and U Iowa, CVC4 aims to support the useful feature set of CVC3 and SMT-LIBv2 while optimizing the design of the core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances. CVC4 represents a completely new code base; it is a from-scratch rewrite of CVC3, and many subsystems have been completely redesigned. Additional decision procedures for CVC4 are currently under development, but for what it currently achieves, it is a lighter-weight and higher-performing tool than CVC3. We describe the system architecture, subsystems of note, and discuss some applications and continuing work.
Reference:
CVC4 (Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, Cesare Tinelli), In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11) (Ganesh Gopalakrishnan, Shaz Qadeer, eds.), Springer, volume 6806, 2011. (Snowbird, Utah)
Bibtex Entry:
@inproceedings{BCD+11,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/BCD+11.pdf",
  author    = "Clark Barrett and Christopher L. Conway and Morgan Deters and
               Liana Hadarean and Dejan Jovanović 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",
  abstract  = "CVC4 is the latest version of the Cooperating Validity Checker. A joint project of NYU and U Iowa, CVC4 aims to support the useful feature set of CVC3 and SMT-LIBv2 while optimizing the design of the core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances. CVC4 represents a completely new code base; it is a from-scratch rewrite of CVC3, and many subsystems have been completely redesigned. Additional decision procedures for CVC4 are currently under development, but for what it currently achieves, it is a lighter-weight and higher-performing tool than CVC3. We describe the system architecture, subsystems of note, and discuss some applications and continuing work."
}

Fork me on GitHub