CVC4” by Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. In Proceedings of the 23^rd International Conference on Computer Aided Verification (CAV '11), (Ganesh Gopalakrishnan and Shaz Qadeer, eds.), July 2011, pp. 171-177. Snowbird, Utah.


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.

BibTeX entry:

   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},
   editor = {Ganesh Gopalakrishnan and Shaz Qadeer},
   title = {{CVC4}},
   booktitle = {Proceedings of the {\it 23^{rd}} International Conference
	on Computer Aided Verification (CAV '11)},
   series = {Lecture Notes in Computer Science},
   volume = {6806},
   pages = {171--177},
   publisher = {Springer},
   month = jul,
   year = {2011},
   note = {Snowbird, Utah},
   url = {}

(This webpage was created with bibtex2web.)