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 条
  • [41] Integrating BDD-based and SAT-based symbolic model checking
    Cimatti, A
    Giunchiglia, E
    Pistore, M
    Roveri, M
    Sebastiani, R
    Tacchella, A
    FRONTIERS OF COMBINING SYSTEMS, 2002, 2309 : 49 - 56
  • [42] SAT-based explicit LTLf satisfiability checking
    Li, Jianwen
    Pu, Geguang
    Zhang, Yueling
    Vardi, Moshe Y.
    Rozier, Kristin Y.
    ARTIFICIAL INTELLIGENCE, 2020, 289
  • [43] Acceleration of SAT-based iterative property checking
    Grosse, D
    Drechsler, R
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 349 - 353
  • [44] SAT-Based Explicit LTLf Satisfiability Checking
    Li, Jianwen
    Rozier, Kristin Y.
    Pu, Geguang
    Zhang, Yueling
    Vardi, Moshe Y.
    THIRTY-THIRD AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTY-FIRST INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / NINTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2019, : 2946 - 2953
  • [45] Incremental deductive & inductive reasoning for SAT-based Bounded Model Checking
    Zhang, L
    Prasad, MR
    Hsiao, MS
    ICCAD-2004: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, IEEE/ACM DIGEST OF TECHNICAL PAPERS, 2004, : 502 - 509
  • [46] SAT-Based Bounded Model Checking for Weighted Deontic Interpreted Systems
    Wozna-Szczesniak, Bozena
    PROGRESS IN ARTIFICIAL INTELLIGENCE, EPIA 2013, 2013, 8154 : 444 - 455
  • [47] COMPLETE SAT-BASED MODEL CHECKING FOR CONTEXT-FREE PROCESSES
    Huang, Geng-Dian
    Wang, Bow-Yaw
    INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2010, 21 (02) : 115 - 134
  • [48] Parallel SAT-Based Parameterised Three-Valued Model Checking
    Timm, Nils
    Gruner, Stefan
    Sibanda, Prince
    MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 : 242 - 259
  • [49] SAT-based Bounded Model Checking forWeighted Deontic Interpreted Systems
    Wozna-Szczesniak, Bozena
    FUNDAMENTA INFORMATICAE, 2016, 143 (1-2) : 173 - 205
  • [50] An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols
    Armando, Alessandro
    Compagna, Luca
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (01) : 91 - 108
12345