Abstract BDDs: A technique for using abstraction in model checking

被引:0
作者
Clarke, E [1 ]
Jha, S [1 ]
Lu, Y [1 ]
Wang, D [1 ]
机构
[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源
CORRECT HARDWARE DESIGN AND VERIFICATION METHODS | 1999年 / 1703卷
关键词
abstract BDDs; model checking; and abstraction;
D O I
暂无
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
We propose a new methodology for exploiting abstraction in the context of model-checking. Our new technique uses abstract BDDs as its underlying data structure. We show that this technique builds a more refined model than traditional compiler-based methods proposed by Clarke, Grumberg and Long. We also provide experimental results to demonstrate the usefulness of our method. We have verified a pipelined carry-save multiplier and a simple version of the PCI local bus protocol. Our verification of the PCI bus revealed a subtle inconsistency in the PCI standard. We believe this is an interesting result by itself.
引用
收藏
页码:172 / 186
页数:15
相关论文
共 50 条
[21]   Combining predicate and numeric abstraction for software model checking [J].
Gurfinkel A. ;
Chaki S. .
International Journal on Software Tools for Technology Transfer, 2010, 12 (06) :409-427
[22]   Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge [J].
Zhou, Conghua ;
Sun, Bo ;
Liu, Zhifeng .
ARTIFICIAL INTELLIGENCE AND COMPUTATIONAL INTELLIGENCE, PT I, 2010, 6319 :209-221
[23]   Abstraction for model checking multi-agent systems [J].
Conghua Zhou ;
Bo Sun ;
Zhifeng Liu .
Frontiers of Computer Science in China, 2011, 5 :14-25
[24]   Boolean and Cartesian abstraction for model checking C programs [J].
Thomas Ball ;
Andreas Podelski ;
Sriram K. Rajamani .
International Journal on Software Tools for Technology Transfer, 2003, 5 (1) :49-58
[25]   Model checking learning agent systems using Promela with embedded C code and abstraction [J].
Kirwan, Ryan ;
Miller, Alice ;
Porr, Bernd .
FORMAL ASPECTS OF COMPUTING, 2016, 28 (06) :1027-1056
[26]   Incompleteness, counterexamples, and refinements in abstract model-checking [J].
Giacobazzi, R ;
Quintarelli, E .
STATIC ANALYSIS, PROCEEDINGS, 2001, 2126 :356-373
[27]   A semantic framework for the abstract model checking of tccp programs [J].
Alpuente, M ;
Gallardo, MD ;
Pimentel, E ;
Villanueva, A .
THEORETICAL COMPUTER SCIENCE, 2005, 346 (01) :58-95
[28]   Directed Model Checking for Fast Abstract Reachability Analysis [J].
Lee, Nakwon ;
Kim, Yunho ;
Kim, Moonzoo ;
Ryu, Duksan ;
Baik, Jongmoon .
IEEE ACCESS, 2021, 9 :158738-158750
[29]   Detecting Spurious Counterexamples Efficiently in Abstract Model Checking [J].
Tian, Cong ;
Duan, Zhenhua .
PROCEEDINGS OF THE 35TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2013), 2013, :202-211
[30]   Model checking, automated abstraction, and compositional verification of Rebeca models [J].
Sirjani, M ;
Movaghar, A ;
Shali, A ;
de Boer, FS .
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2005, 11 (06) :1054-1082