About Cascade
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
Publications
- Christopher L. Conway and Clark Barrett. Verifying Low-Level Implementations of High-Level Datatypes. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, Proceedings of the Twenty-Second International Conference on Computer Aided Verification (CAV '10), volume 6174 of Lecture Notes in Computer Science, pages 306-320. Springer, July 2010. Edinburgh, Scotland.
- 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.
