cascade: C Assertion Checker and Deductive Engine

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 proof that the assertion cannot be violated.

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Nikhil Sethi, Clark Barrett
• Keywords: CAV 2006, Control File, Earlier Stage, Hardware, Multi-stage Verification Strategy