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
PublisherSpringer Verlag
Pages420-422
Number of pages3
Volume9035
ISBN (Print)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)03029743
ISSN (Electronic)16113349

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
CountryUnited Kingdom
CityLondon
Period4/11/154/18/15

Fingerprint

Cascade
Bounded Model Checking
Data storage equipment
Proof of correctness
Program Analysis
Surface mount technology
Memory Model
Model checking
Floating point
Static Analysis
Assertion
Divides
Trace
Partition
Concretes
Standards

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Wang, W., & Barrett, C. (2015). Cascade (Competition contribution). In Tools 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 (Vol. 9035, pp. 420-422). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9035). Springer Verlag. https://doi.org/10.1007/978-3-662-46681-0_33

Cascade (Competition contribution). / Wang, Wei; Barrett, Clark.

Tools 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. Vol. 9035 Springer Verlag, 2015. p. 420-422 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9035).

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

Wang, W & Barrett, C 2015, Cascade (Competition contribution). in Tools 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. vol. 9035, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9035, Springer Verlag, pp. 420-422, 21st 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, 4/11/15. https://doi.org/10.1007/978-3-662-46681-0_33
Wang W, Barrett C. Cascade (Competition contribution). In Tools 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. Vol. 9035. Springer Verlag. 2015. p. 420-422. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-46681-0_33
Wang, Wei ; Barrett, Clark. / Cascade (Competition contribution). Tools 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. Vol. 9035 Springer Verlag, 2015. pp. 420-422 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{51db27468e8241128ed3bc3e5d58d5bf,
title = "Cascade (Competition 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.",
author = "Wei Wang and Clark Barrett",
year = "2015",
doi = "10.1007/978-3-662-46681-0_33",
language = "English (US)",
isbn = "9783662466803",
volume = "9035",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "420--422",
booktitle = "Tools 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",

}

TY - GEN

T1 - Cascade (Competition contribution)

AU - Wang, Wei

AU - Barrett, Clark

PY - 2015

Y1 - 2015

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

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

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

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

U2 - 10.1007/978-3-662-46681-0_33

DO - 10.1007/978-3-662-46681-0_33

M3 - Conference contribution

SN - 9783662466803

VL - 9035

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

SP - 420

EP - 422

BT - Tools 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

PB - Springer Verlag

ER -