“Cascade (Competition Contribution)” by Wei Wang and Clark Barrett. In Proceedings of the 21^st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '15), (Christel Baier and Cesare Tinelli, eds.), Apr. 2015, pp. 420-422. London, United Kingdom.
Cascade is a static program analysis tool developed at New York University. It uses bounded model checking to generate verification conditions and checks them using an SMT solver which either produces a proof of correctness or gives a concrete trace showing how an assertion can fail. It supports the majority of standard C features except for floating point. A distinguishing feature of Cascade is that its analysis uses a memory model which divides up memory into several partitions based on alias information.
BibTeX entry:
@inproceedings{WB15,
author = {Wei Wang and Clark Barrett},
editor = {Christel Baier and Cesare Tinelli},
title = {Cascade (Competition Contribution)},
booktitle = {Proceedings of the {\it 21^{st}} International Conference
on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS '15)},
series = {Lecture Notes in Computer Science},
volume = {9035},
pages = {420--422},
publisher = {Springer},
month = apr,
year = {2015},
note = {London, United Kingdom},
url = {http://theory.stanford.edu/~barrett/pubs/WB15.pdf}
}
(This webpage was created with bibtex2web.)