Hello.

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 trave 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.

Publication

  • Wei Wang, Clark Barrett and Thomas Wies. Cascade 2.0. VMCAI 2014.
  • Christopher L. Conway and Clark Barrett. Verifying Low-Level Implementations of High-Level Datatypes. In 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 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.

Acknowledgement

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