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
Armando, Alessandro
Compagna, Luca
[J]. INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 2008, 7 (01) : 3 - 32
[32] Efficient SAT-based bounded model checking for software verification
Ivancic, Franio
Yang, Zijiang
Ganai, Malay K.
Gupta, Aarti
Ashar, Pranav
[J]. THEORETICAL COMPUTER SCIENCE, 2008, 404 (03) : 256 - 274
[33] On SAT-Based Model Checking of Speed-Independent Circuits
Huemer, Florian
Najvirt, Robert
Steininger, Andreas
[J]. 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
[J]. TASE 2007: FIRST JOINT IEEE/IFIP SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2007, : 339 - +
[35] An analysis of SAT-based model checking techniques in an industrial environment
Amla, N
Du, XQ
Kuehlmann, A
Kurshan, RP
McMillan, KL
[J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 254 - 268
[36] Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking
Ishii, Daisuke
Fujii, Saito
[J]. 2020 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2020), 2020, : 105 - 112
[37] Learning from BDDs in SAT-based bounded model checking
Gupta, A
Ganai, M
Chao, W
Yang, ZJ
Ashar, P
[J]. 40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 824 - 829
[38] State set management for SAT-based unbounded model checking
Chandrasekar, K
Hsiao, MS
[J]. 2005 IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN: VLSI IN COMPUTERS & PROCESSORS, PROCEEDINGS, 2005, : 585 - 590
[39] SAT-based counterexample guided abstraction refinement in model checking
Clarke, EM
[J]. AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 1 - 1
[40] Integrating BDD-based and SAT-based symbolic model checking
Cimatti, A
Giunchiglia, E
Pistore, M
Roveri, M
Sebastiani, R
Tacchella, A
[J]. FRONTIERS OF COMBINING SYSTEMS, 2002, 2309 : 49 - 56

← 1 2 3 4 5 →