“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:
@inproceedings{BCD+11,
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 = {http://theory.stanford.edu/~barrett/pubs/BCD+11.pdf}
}
(This webpage was created with bibtex2web.)