A tool for checking ANSI-C programs

A tool for checking ANSI-C programs
复制标题

DOI：
10.1007/978-3-540-24730-2_15
复制
发表时间：
2004-01-01
期刊：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS
影响因子：
--
通讯作者：
Lerda, F
Lerda, F
中科院分区：
其他
文献类型：
--
作者：
Clarke, E;Kroening, D;Lerda, F

文献摘要

被引文献

相似文献

我们提出了一个工具的ANSI-C程序的形式化验证，使用有界模型检查（BMC）。重点是可用性：该工具支持几乎所有的ANSI-C语言功能，包括指针结构、动态内存分配、递归、浮点和双精度数据类型。从用户的角度来看，验证是高度自动化的：唯一需要的输入是BMC绑定。该工具集成到图形用户界面中。这对于呈现长的反例跟踪是必不可少的：该工具允许单步执行跟踪，就像调试器允许单步执行程序一样。
We present a tool for the formal verification of ANSI-C programs using Bounded Model Checking (BMC). The emphasis is on usability: the tool supports almost all ANSI-C language features, including pointer constructs, dynamic memory allocation, recursion, and the float and double data types. From the perspective of the user, the verification is highly automated: the only input required is the BMC bound. The tool is integrated into a graphical user interface. This is essential for presenting long counterexample traces: the tool allows stepping through the trace in the same way a debugger allows stepping through a program.