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 条
  • [1] Model checking LTL properties over ANSI-C programs with bounded traces
    Jeremy Morse
    Lucas Cordeiro
    Denis Nicole
    Bernd Fischer
    [J]. Software & Systems Modeling, 2015, 14 : 65 - 81
  • [2] Model checking LTL properties over ANSI-C programs with bounded traces
    Morse, Jeremy
    Cordeiro, Lucas
    Nicole, Denis
    Fischer, Bernd
    [J]. SOFTWARE AND SYSTEMS MODELING, 2015, 14 (01): : 65 - 81
  • [3] Loopfrog: A Static Analyzer for ANSI-C Programs
    Kroening, Daniel
    Sharygina, Natasha
    Tonetta, Stefano
    Tsitovich, Aliaksei
    Wintersteiger, Christoph M.
    [J]. 2009 IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 668 - 670
  • [4] Predicate abstraction of ANSI-C programs using SAT
    Clarke, E
    Kroening, D
    Sharygina, N
    Yorav, K
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2004, 25 (2-3) : 105 - 127
  • [5] Hardware verification using ANSI-C programs as a reference
    Clarke, E
    Kroening, D
    [J]. ASP-DAC 2003: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2003, : 308 - 311
  • [6] Predicate Abstraction of ANSI-C Programs Using SAT
    Edmund Clarke
    Daniel Kroening
    Natasha Sharygina
    Karen Yorav
    [J]. Formal Methods in System Design, 2004, 25 : 105 - 127
  • [7] STANDARDIZING ANSI-C
    YOUNG, GA
    [J]. BYTE, 1986, 11 (07): : 14 - 14
  • [8] ADIC: an extensible automatic differentiation tool for ANSI-C
    Bischof, CH
    Roh, L
    Mauer-oats, AJ
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 1997, 27 (12): : 1427 - 1456
  • [9] SMT-Based Bounded Model Checking for Embedded ANSI-C Software
    Cordeiro, Lucas
    Fischer, Bernd
    Marques-Silva, Joao
    [J]. 2009 IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 137 - 148
  • [10] SMT-Based Bounded Model Checking for Embedded ANSI-C Software
    Cordeiro, Lucas
    Fischer, Bernd
    Marques-Silva, Joao
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2012, 38 (04) : 957 - 974
12345