Cascade 2.0
Cascade 2.0
复制标题
级联2.0
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Thomas Wies
中科院分区：
文献类型：
--
作者：
Wen Wang;Clark W. Barrett;Thomas Wies
Cascade是纽约大学开发的程序静态分析工具。Cascade接受一个程序和一个控制文件作为输入。控制文件指定了一个或多个断言，这些断言将与对程序行为的限制一起被检查。该工具为指定的断言生成验证条件，并使用SMT求解器对其进行检查，SMT求解器可以生成证明或给出具体的跟踪，显示断言如何失败。2.0版支持大多数标准C特性，除了浮点。它可以用来验证内存安全性以及用户定义的断言。在本文中，我们描述了级联系统，包括它的一些显着的特点，如它的支持不同的内存模型的权衡精度的可扩展性和它的能力，原因有关的数据结构。
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.