Cascade: C assertion checker and deductive engine

Nikhil Sethi, Clark Barrett

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 18th International Conference, CAV 2006, Proceedings
PublisherSpringer Verlag
Number of pages4
ISBN (Print)354037406X, 9783540374060
StatePublished - 2006
Event18th International Conference on Computer Aided Verification, CAV 2006 - Seattle, WA, United States
Duration: Aug 17 2006Aug 20 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4144 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other18th International Conference on Computer Aided Verification, CAV 2006
Country/TerritoryUnited States
CitySeattle, WA

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Cascade: C assertion checker and deductive engine'. Together they form a unique fingerprint.

Cite this