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
ISBN (Print)9783642540127
DOIs
StatePublished - Jan 1 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)0302-9743
ISSN (Electronic)1611-3349

Other

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

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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 (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