Sciweavers

CAV
2006
Springer

cascade: C Assertion Checker and Deductive Engine

13 years 7 months ago
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.
Nikhil Sethi, Clark Barrett
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CAV
Authors Nikhil Sethi, Clark Barrett
Comments (0)