Interpolation and SAT-based model checking

被引：0
|
作者：
McMillan, KL [1 ]
机构：
[1] Cadence Berkeley Labs, Berkeley, CA USA
来源：
COMPUTER AIDED VERIFICATION | 2003年 / 2725卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We consider a fully SAT-based method of unbounded symbolic model checking based on computing Craig interpolants. In benchmark studies using a set of large industrial circuit verification instances, this method is greatly more efficient than BDD-based symbolic model checking, and compares favorably to some recent SAT-based model checking methods on positive instances.
引用
收藏
页码：1 / 13
页数：13
相关论文
共 50 条
  • [31] SAT-based model-checking for security protocols analysis
    Alessandro Armando
    Luca Compagna
    International Journal of Information Security, 2008, 7 : 3 - 32
  • [32] An analysis of SAT-based model checking techniques in an industrial environment
    Amla, N
    Du, XQ
    Kuehlmann, A
    Kurshan, RP
    McMillan, KL
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 254 - 268
  • [33] On SAT-Based Model Checking of Speed-Independent Circuits
    Huemer, Florian
    Najvirt, Robert
    Steininger, Andreas
    2022 25TH INTERNATIONAL SYMPOSIUM ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS (DDECS), 2022, : 100 - 105
  • [34] Evaluation of SAT-based bounded model checking of ACTL properties
    Xu, Yanyan
    Chen, Wei
    Xu, Liang
    Zhang, Wenhui
    TASE 2007: FIRST JOINT IEEE/IFIP SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2007, : 339 - +
  • [35] Learning from BDDs in SAT-based bounded model checking
    Gupta, A
    Ganai, M
    Chao, W
    Yang, ZJ
    Ashar, P
    40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 824 - 829
  • [36] State set management for SAT-based unbounded model checking
    Chandrasekar, K
    Hsiao, MS
    2005 IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN: VLSI IN COMPUTERS & PROCESSORS, PROCEEDINGS, 2005, : 585 - 590
  • [37] Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking
    Ishii, Daisuke
    Fujii, Saito
    2020 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2020), 2020, : 105 - 112
  • [38] Efficient SAT-based bounded model checking for software verification
    Ivancic, Franio
    Yang, Zijiang
    Ganai, Malay K.
    Gupta, Aarti
    Ashar, Pranav
    THEORETICAL COMPUTER SCIENCE, 2008, 404 (03) : 256 - 274
  • [39] SAT-based model-checking for security protocols analysis
    Armando, Alessandro
    Compagna, Luca
    INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 2008, 7 (01) : 3 - 32
  • [40] SAT-based counterexample guided abstraction refinement in model checking
    Clarke, EM
    AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 1 - 1
12345