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 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.
Awards
- In the 5th International Competition on Software Verification (SV-COMP 2016), Cascade won the bronze medal in the category "Heap".
- In the 4th International Competition on Software Verification (SV-COMP 2015), Cascade won the bronze medal in the category "MemorySafety".
Publications
- Wei Wang, Clark Barrett. "Cascade 2016 (Competition Contribution).
- Wei Wang, Clark Barrett. "Cascade (Competition Contribution). TACAS 2015.
- 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 Google and the National Science Foundation, grant number 0644299.