Cascade: A Code Analyzer, Static Checker, And Deductive Engine

Cascade is a multi-language, multi-paradigm software verification platform. The first two components of Cascade are:

Cascade/C, a precise static analyzer for C programs, intended for use in two-phase analysis.
Cascade/SPL, a library for deductive verification of high-level SPL programs.

People

We are deeply saddened to note the passing of Amir Pnueli. Amir was influential in shaping the work we perform at the Courant Institute and he was instrumental in starting the Cascade project. He is, and will continue to be, sorely missed.

Support

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

Getting the Tool

Running Cascade requires a recent version of the CVC3 SMT solver (nightly builds are available here).

Put the file libcvc3-x.y.z.jar (where x.y.z is the version number of the library) in your Java classpath and the files libcvc3.so and libcvc3jni.so in your dynamic library search path.

Source Code

Core library v0.0.2: (source) (Javadoc)
CVC3 plugin v0.0.1: (source)

The Cascade source code repository is at URL:

https://subversive.cims.nyu.edu/cascade/

To check out a working copy of the core library, just execute

svn co https://subversive.cims.nyu.edu/cascade/trunk/core cascade-core

For the CVC3 plugin, execute

svn co https://subversive.cims.nyu.edu/cascade/trunk/cvc3-plugin cascade-cvc3-plugin

Building the Cascade source requires the Maven build tool. Detailed build instructions are included in the source code.

Maven

The Cascade core library is available as a Maven artifact. The Maven repository for Cascade is:

<repository>
  <id>cascade-public-repo</id>
  <name>Cascade Public Repository</name>
  <url>http://cs.nyu.edu/acsys/cascade/repository/</url>
</repository>

The dependency for the core library is:

<dependency>
  <groupId>edu.nyu.cascade</groupId>
  <artifactId>core</artifactId>
  <version>0.0.1</version>
</dependency>

The dependency for the CVC3 plugin is:

<dependency>
  <groupId>edu.nyu.cascade</groupId>
  <artifactId>cvc3-plugin</artifactId>
  <version>0.0.1</version>
</dependency>

The location of the CVC3 installation can be customized using a local profile. The relevant properties are:

cvc3.version: The full version number of the CVC3 library
cvc3.basedir: The base directory of the CVC3 installation (default: /usr/local)
cvc3.libdir: The directory containing the CVC3 libraries (default ${cvc3.basedir}/lib)
cvc3.libdir: The directory containing the CVC3 JNI bindings (default ${cvc3.libdir}/jni)
cvc3.jar: The path of the CVC3 JAR library (default: ${cvc3.basedir}/java/libcvc3-${cvc3.version}.jar)

Bugs

You can report any bugs to the project Bugzilla page.

Contact: Chris Conway
Last updated: 9 Feb 2010