Cascade: C assertion checker and deductive engine

Nikhil Sethi; Clark Barrett

doi:10.1007/11817963_17

Cascade: C assertion checker and deductive engine

Nikhil Sethi, Clark Barrett

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings
Publisher	Springer Verlag
Pages	166-169
Number of pages	4
ISBN (Print)	354037406X, 9783540374060
DOIs	https://doi.org/10.1007/11817963_17
State	Published - 2006
Event	18th International Conference on Computer Aided Verification, CAV 2006 - Seattle, WA, United States Duration: Aug 17 2006 → Aug 20 2006

Publication series

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

Other

Other	18th International Conference on Computer Aided Verification, CAV 2006
Country/Territory	United States
City	Seattle, WA
Period	8/17/06 → 8/20/06

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/11817963_17

Cite this

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

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

Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings. Springer Verlag, 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 proceeding › Conference contribution

Sethi, N & Barrett, C 2006, Cascade: C assertion checker and deductive engine. in Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4144 LNCS, Springer Verlag, pp. 166-169, 18th International Conference on Computer Aided Verification, CAV 2006, Seattle, WA, United States, 8/17/06. https://doi.org/10.1007/11817963_17

@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",

doi = "10.1007/11817963_17",

language = "English (US)",

isbn = "354037406X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "166--169",

booktitle = "Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings",

}

TY - GEN

T1 - Cascade

T2 - 18th International Conference on Computer Aided Verification, CAV 2006

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

U2 - 10.1007/11817963_17

DO - 10.1007/11817963_17

M3 - Conference contribution

AN - SCOPUS:33749833959

SN - 354037406X

SN - 9783540374060

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

PB - Springer Verlag

Y2 - 17 August 2006 through 20 August 2006

ER -

Cascade: C assertion checker and deductive engine

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this