A tool for checking ANSI-C programs

被引：748
|
作者：
Clarke, E [1 ]
Kroening, D [1 ]
Lerda, F [1 ]
机构：
[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS | 2004年 / 2988卷
关键词：
D O I：
10.1007/978-3-540-24730-2_15
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：168 / 176
页数：9
相关论文
共 50 条
  • [21] Implementation of the memory-safe full ANSI-C compiler
    Research Center for Information Security , National Institute of Advanced Industrial Science and Technology , Japan
    [J]. Proc ACM SIGPLAN Conf Program Lang Des Implementation PLDI, (259-269): : 259 - 269
  • [22] ANSI-C实现面向对象编程及应用
    赵辉
    屈雷
    [J]. 咸阳师范学院学报, 2015, 30 (06) : 61 - 64
  • [23] Methodological considerations for automatic synthesis of fuzzy processors in ANSI-C
    Forero, Edgar
    Garcia, Edgar
    Melgarejo, Miguel
    [J]. INGENIERIA, 2009, 14 (01): : 53 - 58
  • [24] GOING FROM K-AND-R TO ANSI-C
    LADD, SR
    [J]. DR DOBBS JOURNAL, 1989, 14 (08): : 74 - &
  • [25] Implementation of the Memory-safe Full ANSI-C Compiler
    Oiwa, Yutaka
    [J]. PLDI'09 PROCEEDINGS OF THE 2009 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2009, : 259 - 269
  • [26] SATABS: SAT-based predicate abstraction for ANSI-C
    Clarke, E
    Kroening, D
    Sharygina, N
    Yorav, K
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 570 - 574
  • [27] Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis
    Rieder, Bernhard
    Puschner, Peter
    Wenzel, Ingomar
    [J]. PROCEEDINGS OF THE SIXTH INTERNATIONAL WORKSHOP ON INTELLIGENT SOLUTIONS IN EMBEDDED SYSTEMS, 2008, : 3 - 9
  • [28] Implementation of the Memory-safe Full ANSI-C Compiler
    Oiwa, Yutaka
    [J]. ACM SIGPLAN NOTICES, 2009, 44 (06) : 259 - 269
  • [29] COMPUTING A-STAR-B (MOD-N) EFFICIENTLY IN ANSI-C
    BAKER, HG
    [J]. SIGPLAN NOTICES, 1992, 27 (01): : 95 - 98
  • [30] FocusCheck: A tool for model checking and debugging sequential C programs
    Keller, CW
    Saha, D
    Basu, S
    Smolka, SA
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 563 - 569
12345