Disk based software verification via bounded model checking

被引：2
作者：
Brizzolari, Fernando [1 ]
Melatti, Igor [1 ]
Tronci, Enrico [1 ]
Della Penna, Giuseppe [2 ]
机构：
[1] Univ Roma La Sapienza, Dept Comp Sci, I-00198 Rome, Italy
[2] Univ Aquila, Dept Comp Sci, I-67010 Coppito, Italy
来源：
14TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS | 2007年
关键词：
D O I：
10.1109/ASPEC.2007.55
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
One of the most succesfull approach to automatic software verification is SAT based Bounded Model Checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC.
引用
收藏
页码：358 / +
页数：2
相关论文
共 39 条
  • [1] Aho Alfred V., 1986, ADDISON WESLEY SERIE
  • [2] Automatic symbolic verification of embedded systems
    Alur, R
    Henzinger, TA
    Ho, PH
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1996, 22 (03) : 181 - 201
  • [3] ALUR R, 2001, P ICSE 01
  • [4] [Anonymous], 1990, Introduction to Algorithms
  • [5] [Anonymous], 2003, SC 03
  • [6] Bacchus F, 2004, LECT NOTES COMPUT SC, V2919, P341
  • [7] BEREZIN S, 1998, P COMPOS 97, P81
  • [8] Biere A, 2003, ADV COMPUT, V58, P117
  • [9] Biere A, 1999, LECT NOTES COMPUT SC, V1579, P193
  • [10] A simplifier for propositional formulas with many binary clauses
    Brafman, RI
    [J]. IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART B-CYBERNETICS, 2004, 34 (01): : 52 - 59
1234