Difference between revisions of "About Cascade"

Revision as of 11:49, 19 December 2012

Cascade is a tool to check assertions in C programs as part of multi-stage verification strategy. There are a number of static analysis tools which can analyse large programs and find potential bugs. To scale, these tools must abstract the programs with the result that some of the errors reported are often false. Having to check these false alarms is often a time consuming task.

In two stage verification, a light-weight analysis capable of scaling to large codes is first run to detect potential bugs. Then a more detailed analysis is used to rule out false errors. Cascade provides a generic back-end for two stage verification of C programs which can be easily integrated with any initial stage. Cascade can handle most C constructs like loops, functions (including recursive functions), structs, pointers, and dynamic memory allocation.

Cascade uses a control file to interface with the first stage tool. The control file specifies the assertion(s) to be checked. In addition, the control file can be used to constrain the search for a violating trace by restricting the program paths to be explored or giving constraints on program variables.

People

• Clark Barrett
• Chris Conway
• Dejan Jovanović
• Wei Wang

Publications

Nikhil Sethi and Clark Barrett. CASCADE: C Assertion Checker and Deductive Engine. In Thomas Ball and Robert B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV '06), volume 4144 of Lecture Notes in Computer Science, pages 166-169. Springer-Verlag, August 2006. Seattle, Washington.

Support

Cascade development is supported by the National Science Foundation, grant number 0644299.