Cascade (Competition contribution)

Wei Wang, Clark Barrett

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

Abstract

Cascade is a static program analysis tool developed at New York University. It uses bounded model checking to generate verification conditions and checks them using an SMT solver which either produces a proof of correctness or gives a concrete trace showing how an assertion can fail. It supports the majority of standard C features except for floating point. A distinguishing feature of Cascade is that its analysis uses a memory model which divides up memory into several partitions based on alias information.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
EditorsCesare Tinelli, Christel Baier
PublisherSpringer Verlag
Pages420-422
Number of pages3
ISBN (Electronic)9783662466803
DOIs
StatePublished - 2015
Event21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
Duration: Apr 11 2015Apr 18 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9035
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
Country/TerritoryUnited Kingdom
CityLondon
Period4/11/154/18/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Cascade (Competition contribution)'. Together they form a unique fingerprint.

Cite this