“Cascade 2.0” by Wei Wang, Clark Barrett, and Thomas Wies. In Proceedings of the 15^th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '14), (Kenneth L. McMillan and Xavier Rival, eds.), Jan. 2014, pp. 142-160. San Diego, California.
Cascade is a program static analysis tool developed at New York University. Cascade takes as input a program and a control file. The control file specifies one or more assertions to be checked together with restrictions on program behaviors. The tool generates verification conditions for the specified assertions and checks them using an SMT solver which either produces a proof or gives a concrete trace showing how an assertion can fail. Version 2.0 supports the majority of standard C features except for floating point. It can be used to verify both memory safety as well as user-defined assertions. In this paper, we describe the Cascade system including some of its distinguishing features such as its support for different memory models (trading off precision for scalability) and its ability to reason about linked data structures.
BibTeX entry:
@inproceedings{WBW14,
author = {Wei Wang and Clark Barrett and Thomas Wies},
editor = {Kenneth L. McMillan and Xavier Rival},
title = {Cascade 2.0},
booktitle = {Proceedings of the {\it 15^{th}} International Conference
on Verification, Model Checking, and Abstract Interpretation
(VMCAI '14)},
series = {Lecture Notes in Computer Science},
volume = {8318},
pages = {142--160},
publisher = {Springer Berlin Heidelberg},
month = jan,
year = {2014},
note = {San Diego, California},
url = {http://theory.stanford.edu/~barrett/pubs/WBW14.pdf}
}
(This webpage was created with bibtex2web.)