Cascade is an open source C program static analysis tool developed at New York University. Cascade takes as input a C 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 violating an assertion.

Cascade 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. The latest version includes a new feature which incorporates constructs into the assertion language for reasoning about linked data structures.




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