View source for About Cascade

From CVC4

You do not have permission to edit this page, for the following reason:

The action you have requested is limited to users in the group: Users.

You can view and copy the source of this page.

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 ==
* [http://www.cs.nyu.edu/~barrett/ Clark Barrett]
* [http://www.cs.nyu.edu/~cconway/ Chris Conway]
* [http://www.cs.nyu.edu/~dejan/ Dejan Jovanović]
* [http://www.cs.wustl.edu/~mdeters/ Morgan Deters]
* [http://www.cs.nyu.edu/pnueli Amir Pnueli]
* [http://www.cs.nyu.edu/~nsethi Nikhil Sethi]
* [http://www.cs.nyu.edu/~wwang1109/ Wei Wang]

== Publications ==
* Christopher L. Conway and Clark Barrett. [http://www.cs.nyu.edu/~cconway/papers/conway-2010-datatypes.pdf 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. [http://cs.nyu.edu/~barrett/pubs/SB06.ps 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.

Return to About Cascade.

Retrieved from "http://cvc4.cs.stanford.edu/wiki/About_Cascade"

View source for About Cascade

Navigation menu

Views

Personal tools

CVC4

For CVC4 Developers

Cascade

Meta

Wiki

Search

Tools