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 条
  • [1] Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
    Beyer, Dirk
    Lee, Nian-Ze
    Wendler, Philipp
    JOURNAL OF AUTOMATED REASONING, 2025, 69 (01)
  • [2] SAT-based Model Checking: Interpolation, IC3, and Beyond
    Grumberg, Orna
    Shoham, Sharon
    Vizel, Yakir
    SOFTWARE SYSTEMS SAFETY, 2014, 36 : 17 - 41
  • [3] Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
    G. Cabodi
    P. E. Camurati
    M. Palena
    P. Pasini
    Formal Methods in System Design, 2022, 60 : 117 - 146
  • [4] Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
    Cabodi, G.
    Camurati, P. E.
    Palena, M.
    Pasini, P.
    FORMAL METHODS IN SYSTEM DESIGN, 2022, 60 (02) : 117 - 146
  • [5] Interpolation with Guided Refinement: revisiting incrementality in SAT-based Unbounded Model Checking
    Cabodi, G.
    Palena, M.
    Pasini, P.
    2014 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2014, : 43 - 50
  • [6] SAT-Based Model Checking without Unrolling
    Bradley, Aaron R.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2011, 6538 : 70 - 87
  • [7] Sat-based model checking for region automata
    Yu, Fang
    Wang, Bow-Yaw
    INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2006, 17 (04) : 775 - 795
  • [8] Symmetry reduction in SAT-based model checking
    Tang, DJ
    Malik, S
    Gupta, A
    Ip, CN
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2005, 3576 : 125 - 138
  • [9] SAT-based unbounded symbolic model checking
    Kang, HJ
    Park, IC
    40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 840 - 843
  • [10] Certifying proofs for SAT-based model checking
    Alberto Griggio
    Marco Roveri
    Stefano Tonetta
    Formal Methods in System Design, 2021, 57 : 178 - 210
12345