@inproceedings{1f43ca2ac25f4da28d5c8927a2ef98b7,
title = "Cascade 2.0",
abstract = "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.",
author = "Wei Wang and Clark Barrett and Thomas Wies",
year = "2014",
doi = "10.1007/978-3-642-54013-4_9",
language = "English (US)",
isbn = "9783642540127",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "142--160",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings",
note = "15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014 ; Conference date: 20-01-2014 Through 21-01-2014",
}