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 条

[21] Improvement of SAT-based Model Checking of Security Protocols
Yang, Yuanyuan
Ma, Wenping
2009 INTERNATIONAL CONFERENCE ON E-BUSINESS AND INFORMATION SYSTEM SECURITY, VOLS 1 AND 2, 2009, : 223 - 227
[22] SAT-based unbounded model checking of timed automata
Penczek, Wojciech
Szreter, Maciej
SEVENTH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2007, : 236 - 237
[23] Efficient LTL compilation for SAT-based model checking
Armoni, R
Egorov, S
Fraer, R
Korchemny, D
Vardi, MY
ICCAD-2005: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, DIGEST OF TECHNICAL PAPERS, 2005, : 877 - 884
[24] Model checking with SAT-based characterization of ACTL formulas
Zhang, Wenhui
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4789 : 191 - 211
[25] Combining abstraction refinement and SAT-Based model checking
Amla, Nina
McMillan, Kenneth L.
Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, 2007, 4424 : 405 - 419
[26] Proving ∀μ-calculus properties with SAT-based model checking
Wang, BY
FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 113 - 127
[27] Frontend model generation for SAT-based property checking
Wedler, M
Stoffel, D
Kunz, W
2005 6TH INTERNATIONAL CONFERENCE ON ASIC PROCEEDINGS, BOOKS 1 AND 2, 2005, : 914 - 919
[28] SAT-Based ATL Satisfiability Checking
Kacprzak, Magdalena
Niewiadomski, Artur
Penczek, Wojciech
KR2020: PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2020, : 539 - 549
[29] Lazy Abstraction and SAT-Based Reachability in Hardware Model Checking
Vizel, Yakir
Grumberg, Orna
Shoham, Sharon
PROCEEDINGS OF THE 12TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2012), 2012, : 173 - 181
[30] SAT-based bounded model checking for SE-LTL
Zhou Conghua
Ju Shiguang
SNPD 2007: EIGHTH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, ARTIFICIAL INTELLIGENCE, NETWORKING, AND PARALLEL/DISTRIBUTED COMPUTING, VOL 3, PROCEEDINGS, 2007, : 582 - +

← 1 2 3 4 5 →