CASCADE: C Assertion Checker and Deductive Engine

“CASCADE: C Assertion Checker and Deductive Engine” by Nikhil Sethi and Clark Barrett. In Proceedings of the 18^th International Conference on Computer Aided Verification (CAV '06), (Thomas Ball and Robert B. Jones, eds.), Aug. 2006, pp. 166-169. Seattle, Washington.

Abstract

We present a tool, called Cascade, to check assertions in C programs as part of a multi-stage verification strategy. Cascade takes as input a C program and a control file (the output of an earlier stage) that specifies one or more assertions to be checked together with (optionally) some restrictions on program behaviors. For each assertion, Cascade produces either a concrete trace violating the assertion or a deduction (proof) that the assertion cannot be violated.

BibTeX entry:

@inproceedings{SB06,
   author = {Nikhil Sethi and Clark Barrett},
   editor = {Thomas Ball and Robert B. Jones},
   title = {{CASCADE}: C Assertion Checker and Deductive Engine},
   booktitle = {Proceedings of the {\it 18^{th}} International Conference
	on Computer Aided Verification (CAV '06)},
   series = {Lecture Notes in Computer Science},
   volume = {4144},
   pages = {166--169},
   publisher = {Springer-Verlag},
   month = aug,
   year = {2006},
   note = {Seattle, Washington},
   url = {http://theory.stanford.edu/~barrett/pubs/SB06.pdf}
}

(This webpage was created with bibtex2web.)