Cascade 2.0

Wei Wang, Clark Barrett, Thomas Wies

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

Abstract

Cascade is a program static analysis tool developed at New York University. Cascade takes as input a program and a control file. The control file specifies one or more assertions to be checked together with restrictions on program behaviors. The tool generates verification conditions for the specified assertions and checks them using an SMT solver which either produces a proof or gives a concrete trace showing how an assertion can fail. Version 2.0 supports the majority of standard C features except for floating point. It can be used to verify both memory safety as well as user-defined assertions. In this paper, we describe the Cascade system including some of its distinguishing features such as its support for different memory models (trading off precision for scalability) and its ability to reason about linked data structures.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings
PublisherSpringer Verlag
Pages142-160
Number of pages19
Volume8318 LNCS
ISBN (Print)9783642540127
DOIs
StatePublished - 2014
Event15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014 - San Diego, CA, United States
Duration: Jan 20 2014Jan 21 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8318 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014
CountryUnited States
CitySan Diego, CA
Period1/20/141/21/14

Fingerprint

Assertion
Cascade
Data storage equipment
Surface mount technology
Static analysis
Data structures
Scalability
Concretes
Linked Data
Program Analysis
Memory Model
Floating point
Static Analysis
Data Structures
Safety
Trace
Verify
Restriction

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Wang, W., Barrett, C., & Wies, T. (2014). Cascade 2.0. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings (Vol. 8318 LNCS, pp. 142-160). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8318 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-54013-4_9

Cascade 2.0. / Wang, Wei; Barrett, Clark; Wies, Thomas.

Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings. Vol. 8318 LNCS Springer Verlag, 2014. p. 142-160 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8318 LNCS).

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

Wang, W, Barrett, C & Wies, T 2014, Cascade 2.0. in Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings. vol. 8318 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8318 LNCS, Springer Verlag, pp. 142-160, 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014, San Diego, CA, United States, 1/20/14. https://doi.org/10.1007/978-3-642-54013-4_9
Wang W, Barrett C, Wies T. Cascade 2.0. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings. Vol. 8318 LNCS. Springer Verlag. 2014. p. 142-160. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-54013-4_9
Wang, Wei ; Barrett, Clark ; Wies, Thomas. / Cascade 2.0. Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings. Vol. 8318 LNCS Springer Verlag, 2014. pp. 142-160 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{1f43ca2ac25f4da28d5c8927a2ef98b7,
title = "Cascade 2.0",
abstract = "Cascade is a program static analysis tool developed at New York University. Cascade takes as input a program and a control file. The control file specifies one or more assertions to be checked together with restrictions on program behaviors. The tool generates verification conditions for the specified assertions and checks them using an SMT solver which either produces a proof or gives a concrete trace showing how an assertion can fail. Version 2.0 supports the majority of standard C features except for floating point. It can be used to verify both memory safety as well as user-defined assertions. In this paper, we describe the Cascade system including some of its distinguishing features such as its support for different memory models (trading off precision for scalability) and its ability to reason about linked data structures.",
author = "Wei Wang and Clark Barrett and Thomas Wies",
year = "2014",
doi = "10.1007/978-3-642-54013-4_9",
language = "English (US)",
isbn = "9783642540127",
volume = "8318 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "142--160",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings",

}

TY - GEN

T1 - Cascade 2.0

AU - Wang, Wei

AU - Barrett, Clark

AU - Wies, Thomas

PY - 2014

Y1 - 2014

N2 - Cascade is a program static analysis tool developed at New York University. Cascade takes as input a program and a control file. The control file specifies one or more assertions to be checked together with restrictions on program behaviors. The tool generates verification conditions for the specified assertions and checks them using an SMT solver which either produces a proof or gives a concrete trace showing how an assertion can fail. Version 2.0 supports the majority of standard C features except for floating point. It can be used to verify both memory safety as well as user-defined assertions. In this paper, we describe the Cascade system including some of its distinguishing features such as its support for different memory models (trading off precision for scalability) and its ability to reason about linked data structures.

AB - Cascade is a program static analysis tool developed at New York University. Cascade takes as input a program and a control file. The control file specifies one or more assertions to be checked together with restrictions on program behaviors. The tool generates verification conditions for the specified assertions and checks them using an SMT solver which either produces a proof or gives a concrete trace showing how an assertion can fail. Version 2.0 supports the majority of standard C features except for floating point. It can be used to verify both memory safety as well as user-defined assertions. In this paper, we describe the Cascade system including some of its distinguishing features such as its support for different memory models (trading off precision for scalability) and its ability to reason about linked data structures.

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

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

U2 - 10.1007/978-3-642-54013-4_9

DO - 10.1007/978-3-642-54013-4_9

M3 - Conference contribution

AN - SCOPUS:84958520621

SN - 9783642540127

VL - 8318 LNCS

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

SP - 142

EP - 160

BT - Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings

PB - Springer Verlag

ER -