Cascade (Competition Contribution)

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, UK.

Abstract

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, UK},
   url = {http://www.cs.nyu.edu/~barrett/pubs/WB15.pdf}
}

(This webpage was created with bibtex2web.)