About Cascade - Revision history

Wwang: /* People */

2012-12-19T19:52:50Z

‎People

Wwang: /* Publications */

2012-12-19T19:51:11Z

‎Publications

Wwang: /* Publications */

2012-12-19T19:50:46Z

‎Publications

Wwang: /* Publications */

2012-12-19T19:49:32Z

‎Publications

Wwang: /* Support */

2012-12-19T19:48:39Z

‎Support

Wwang: /* People */

2012-12-19T19:46:44Z

‎People

Wwang: /* People */

2012-12-17T05:42:18Z

‎People

Wwang: /* People */

2012-12-17T05:41:41Z

‎People

Wwang at 05:38, 17 December 2012

2012-12-17T05:38:10Z

Wwang at 17:54, 12 December 2012

2012-12-12T17:54:35Z

@@ Line 9: / Line 9: @@
 * [http://www.cs.nyu.edu/~cconway/ Chris Conway]
 * [http://www.cs.nyu.edu/~dejan/ Dejan Jovanović]
 * [http://www.cs.nyu.edu/~wwang1109/ Wei Wang]

@@ Line 12: / Line 12: @@
 == Publications ==
-* Christopher L. Conway and Clark Barrett. [https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CDcQFjAA&url=http%3A%2F%2Fwww.cs.nyu.edu%2F~cconway%2Fpapers%2Fconway-2010-datatypes.pdf&ei=ihrSULiSJa-70QHKo4GgCw&usg=AFQjCNGMR4KKLfP4NPx0liddH4ChtZXkbQ&sig2=D37AJMBY2rPGU-LrcDcrug&bvm=bv.1355534169,d.dmQ 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.
+* 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.

@@ Line 12: / Line 12: @@
 == Publications ==
-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.
+* Christopher L. Conway and Clark Barrett. [https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CDcQFjAA&url=http%3A%2F%2Fwww.cs.nyu.edu%2F~cconway%2Fpapers%2Fconway-2010-datatypes.pdf&ei=ihrSULiSJa-70QHKo4GgCw&usg=AFQjCNGMR4KKLfP4NPx0liddH4ChtZXkbQ&sig2=D37AJMBY2rPGU-LrcDcrug&bvm=bv.1355534169,d.dmQ 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.
 == Support ==
 Cascade development is supported by the National Science Foundation, grant number 0644299.

@@ Line 12: / Line 12: @@
 == Publications ==
-Nikhil Sethi and Clark Barrett. 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.
+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.

@@ Line 10: / Line 10: @@
 * [http://www.cs.nyu.edu/~dejan/ Dejan Jovanović]
 * [http://www.cs.nyu.edu/~wwang1109/ Wei Wang]
 == Support ==
 Cascade development is supported by the National Science Foundation, grant number 0644299.

← Older revision		Revision as of 19:46, 19 December 2012
Line 10:		Line 10:
	* [http://www.cs.nyu.edu/~dejan/ Dejan Jovanović]		* [http://www.cs.nyu.edu/~dejan/ Dejan Jovanović]
	* [http://www.cs.nyu.edu/~wwang1109/ Wei Wang]		* [http://www.cs.nyu.edu/~wwang1109/ Wei Wang]
		+
		+	== Support ==
		+	Cascade development is supported by the National Science Foundation, grant number 0644299.

← Older revision		Revision as of 05:41, 17 December 2012
Line 9:		Line 9:
	* [http://www.cs.nyu.edu/~cconway/ Chris Conway]		* [http://www.cs.nyu.edu/~cconway/ Chris Conway]
	* [http://www.cs.nyu.edu/~dejan/ Dejan Jovanović]		* [http://www.cs.nyu.edu/~dejan/ Dejan Jovanović]
		+	* [http://www.cs.nyu.edu/pnueli/ Amir Pnueli]
		+	* [http://www.cs.nyu.edu/~nsethi Nikhil Sethi]
		+	* [http://www.cs.nyu.edu/~wwang1109/ Wei Wang]

← Older revision		Revision as of 05:38, 17 December 2012
Line 4:		Line 4:

	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.		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ć]

@@ Line 1: / Line 1: @@
-Cascade/C 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.
+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/C provides a generic back-end for two stage verification of C programs which can be easily integrated with any initial stage. Cascade/C can handle most C constructs like loops, functions (including recursive functions), structs, pointers, and dynamic memory allocation.
+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/C 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.
+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.