Integrating BDD-based and SAT-based symbolic model checking

被引：0

作者：

Cimatti, A

Giunchiglia, E

Pistore, M

Roveri, M

Sebastiani, R

Tacchella, A

机构：

[1] IRST, ITC, I-38050 Trento, Italy

[2] Univ Genoa, DIST, I-16145 Genoa, Italy

[3] Univ Trent, I-38050 Trento, Italy

来源：

FRONTIERS OF COMBINING SYSTEMS | 2002年 / 2309卷

关键词：

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Symbolic model checking is a very successful formal verification technique, classically based on Binary Decision Diagrams (BDDs). Recently, propositional satisfiability (SAT) techniques have been proposed as a computational basis for symbolic model checking, and proved to be an effective alternative to BDD-based techniques. In this paper we show how BDD-based and SAT-based techniques have been effectively integrated within the NuSMV symbolic model, checker.

引用

页码：49 / 56

页数：8

共 50 条

[1] Improving SAT-based Bounded Model Checking by means of BDD-based approximate traversals
Cabodi, G
Nocco, S
Quer, S
[J]. JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2004, 10 (12) : 1693 - 1730
[2] Improving SAT-based bounded model checking by means of BDD-based approximate traversals
Cabodi, G
Nocco, S
Quer, S
[J]. DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, PROCEEDINGS, 2003, : 898 - 903
[3] SAT-based unbounded symbolic model checking
Kang, HJ
Park, IC
[J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2005, 24 (02) : 129 - 140
[4] SAT-based unbounded symbolic model checking
Kang, HJ
Park, IC
[J]. 40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 840 - 843
[5] Tightening BDD-based Approximate Reachability with SAT-based Clause Generalization
Cabodi, G.
Pasini, P.
Quer, S.
Vendraminetto, D.
[J]. 2014 DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION (DATE), 2014,
[6] Distributed BDD-Based Model Checking
Grumberg, Orna
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (72): : 29 - +
[7] Interpolation and SAT-based model checking
McMillan, KL
[J]. COMPUTER AIDED VERIFICATION, 2003, 2725 : 1 - 13
[8] Efficient SAT-based unbounded symbolic model checking using circuit cofactoring
Ganai, MK
Gupta, A
Ashar, P
[J]. ICCAD-2004: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, IEEE/ACM DIGEST OF TECHNICAL PAPERS, 2004, : 510 - 517
[9] Certifying proofs for SAT-based model checking
Griggio, Alberto
Roveri, Marco
Tonetta, Stefano
[J]. FORMAL METHODS IN SYSTEM DESIGN, 2021, 57 (02) : 178 - 210
[10] Sat-based model checking for region automata
Yu, Fang
Wang, Bow-Yaw
[J]. INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2006, 17 (04) : 775 - 795

← 1 2 3 4 5 →