Using bounded model checking with BOGOR

被引：0

作者：

Lee, Taehoon ^{[1
]}

Cho, Mintaek ^{[1
]}

Kwon, Gihwon ^{[1
]}

机构：

[1] Kyonggi Univ, Dept Comp Sci, Suwon, Kyonggi Do, South Korea

来源：

SERA 2007: 5TH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH, MANAGEMENT, AND APPLICATIONS, PROCEEDINGS | 2007年

关键词：

D O I：

10.1109/SERA.2007.106

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

BOGOR model checking framework is developed for Object-Oriented software verification. It represents system as BIR (Bandera Intermediate Language). To model checking BIR, the BOGOR represents state as a node and transition as edge. First, BOGOR generates node and edge. Second, Model checking is performed in graph structure. However, this approach is inefficient to verify large software system. In this paper, we present symbolic model checking techniques to verify efficient BIR model checking. Experimental results show that the proposed algorithm can check more efficiently.

引用

页码：863 / +

页数：2

共 50 条

[1] Domain-specific model checking using the Bogor framework
Robby
Dwyer, Matthew B.
Hatcliff, John
[J]. ASE 2006: 21ST IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2006, : 369 - +
[2] Symbolic Causality Checking Using Bounded Model Checking
Beer, Adrian
Heidinger, Stephan
Kuehne, Uwe
Leitner-Fischer, Florian
Leue, Stefan
[J]. MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 : 203 - 221
[3] Bounded model checking using satisfiability solving
Clarke, E
Biere, A
Raimi, R
Zhu, Y
[J]. FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (01) : 7 - 34
[4] Bounded Model Checking Using Satisfiability Solving
Edmund Clarke
Armin Biere
Richard Raimi
Yunshan Zhu
[J]. Formal Methods in System Design, 2001, 19 : 7 - 34
[5] Bounded model checking
Biere, Armin
[J]. Frontiers in Artificial Intelligence and Applications, 2009, 185 (01) : 457 - 481
[6] Bounded Model Checking
Biere, A
Cimatti, A
Clarke, EM
Strichman, O
Zhu, YS
[J]. ADVANCES IN COMPUTERS, VOL 58: HIGHLY DEPENDABLE SOFTWARE, 2003, 58 : 117 - 148
[7] Towards automated software model checking using graph transformation systems and Bogor
Rafe, Vahid
Rahmani, Adel T.
[J]. JOURNAL OF ZHEJIANG UNIVERSITY-SCIENCE A, 2009, 10 (08): : 1093 - 1105
[8] Towards automated software model checking using graph transformation systems and Bogor
Vahid Rafe
Adel T. Rahmani
[J]. Journal of Zhejiang University-SCIENCE A, 2009, 10 : 1093 - 1105
[9] Towards automated software model checking using graph transformation systems and Bogor
Vahid RAFE
Adel T.RAHMANI
[J]. Journal of Zhejiang University(Science A:An International Applied Physics & Engineering Journal)., 2009, 10 (08) - 1105
[10] Checking nested properties using bounded model checking and sequential ATPG
Qiang, Q
Saab, DG
Abraham, JA
[J]. 19TH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 2005, : 225 - 230

← 1 2 3 4 5 →