SATABS: SAT-based predicate abstraction for ANSI-C

被引：0
|
作者：
Clarke, E [1 ]
Kroening, D
Sharygina, N
Yorav, K
机构：
[1] Carnegie Mellon Univ, Sch Comp Sci, Pittsburgh, PA 15213 USA
[2] ETH, Zurich, Switzerland
[3] Carnegie Mellon Univ, Inst Software Engn, Pittsburgh, PA 15213 USA
[4] IBM Corp, Haifa, Israel
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS | 2005年 / 3440卷
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper presents a model checking tool, SATABS, that implements a predicate abstraction refinement loop. Existing software verification tools such as SLAM, BLAST, or MAGIC use decision procedures for abstraction and simulation that are limited to integers. SATABS overcomes these limitations by using a SAT-solver. This allows the model checker to handle the semantics of the ANSI-C standard accurately. This includes a sound treatment of bit-vector overflow, and of the ANSI-C pointer arithmetic constructs.
引用
收藏
页码：570 / 574
页数：5
相关论文
共 50 条
  • [1] 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
  • [2] 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
  • [3] Core Minimization in SAT-based Abstraction
    Belov, Anton
    Chen, Huan
    Mishchenko, Alan
    Marques-Silva, Joao
    [J]. DESIGN, AUTOMATION & TEST IN EUROPE, 2013, : 1411 - 1416
  • [4] SAT based predicate abstraction for hardware verification
    Clarke, E
    Talupur, M
    Veith, H
    Wang, D
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 : 78 - 92
  • [5] SAT-based counterexample guided abstraction refinement
    Clarke, EM
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 1 - 1
  • [6] STANDARDIZING ANSI-C
    YOUNG, GA
    [J]. BYTE, 1986, 11 (07): : 14 - 14
  • [7] Dynamic abstraction using SAT-based BMC
    Zhang, L
    Prasad, MR
    Hsiao, MS
    Sidle, T
    [J]. 42ND DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2005, 2005, : 754 - 757
  • [8] A RETARGETABLE COMPILER FOR ANSI-C
    FRASER, CW
    HANSON, DR
    [J]. SIGPLAN NOTICES, 1991, 26 (10): : 29 - 43
  • [9] Abstraction and BDDs complement SAT-based BMC in DiVer
    Gupta, A
    Ganai, M
    Wang, C
    Yang, ZJ
    Ashar, P
    [J]. COMPUTER AIDED VERIFICATION, 2003, 2725 : 206 - 209
  • [10] Combining abstraction refinement and SAT-Based model checking
    Amla, Nina
    McMillan, Kenneth L.
    [J]. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, 2007, 4424 : 405 - 419
12345