Cascade: C assertion checker and deductive engine

Nikhil Sethi, Clark Barrett

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

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 18th International Conference, CAV 2006, Proceedings
Pages166-169
Number of pages4
Volume4144 LNCS
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)03029743
ISSN (Electronic)16113349

Other

Other18th International Conference on Computer Aided Verification, CAV 2006
CountryUnited States
CitySeattle, WA
Period8/17/068/20/06

Fingerprint

Assertion
Cascade
Engine
Concretes
Engines
Deduction
Trace
Restriction
Output

ASJC Scopus subject areas

  • Biochemistry, Genetics and Molecular Biology(all)
  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Sethi, N., & Barrett, C. (2006). Cascade: C assertion checker and deductive engine. In Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings (Vol. 4144 LNCS, pp. 166-169). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4144 LNCS).

Cascade : C assertion checker and deductive engine. / Sethi, Nikhil; Barrett, Clark.

Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings. Vol. 4144 LNCS 2006. p. 166-169 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4144 LNCS).

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

Sethi, N & Barrett, C 2006, Cascade: C assertion checker and deductive engine. in Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings. vol. 4144 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4144 LNCS, pp. 166-169, 18th International Conference on Computer Aided Verification, CAV 2006, Seattle, WA, United States, 8/17/06.
Sethi N, Barrett C. Cascade: C assertion checker and deductive engine. In Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings. Vol. 4144 LNCS. 2006. p. 166-169. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Sethi, Nikhil ; Barrett, Clark. / Cascade : C assertion checker and deductive engine. Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings. Vol. 4144 LNCS 2006. pp. 166-169 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{1f37e931f69f4ed3b8c55368c5d34474,
title = "Cascade: C assertion checker and deductive engine",
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.",
author = "Nikhil Sethi and Clark Barrett",
year = "2006",
language = "English (US)",
isbn = "354037406X",
volume = "4144 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "166--169",
booktitle = "Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings",

}

TY - GEN

T1 - Cascade

T2 - C assertion checker and deductive engine

AU - Sethi, Nikhil

AU - Barrett, Clark

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33749833959&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33749833959&partnerID=8YFLogxK

M3 - Conference contribution

SN - 354037406X

SN - 9783540374060

VL - 4144 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 166

EP - 169

BT - Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings

ER -