Proceedings of the 2nd International Conference on Computer Science and Electronics Engineering (ICCSEE 2013)

<Previous Article In Volume
Next Article In Volume>

Incremental Semantic LTL Bounded Model Checking

Authors
Rui Wang, Wanwei Liu, Xiaoguang Mao, Tun Li
Corresponding Author
Rui Wang
Available Online March 2013.
DOI
10.2991/iccsee.2013.237How to use a DOI?
Keywords
bounded model checking, semantic encoding, incremental, NuSMV
Abstract

Bounded model checking has proven to be an efficient method for finding bugs in system designs. In this paper, we present an incremental semantic translation for Bounded model checking and give an incremental algorithm. We implement this method in NuSMV model checker and report encouraging results.

Copyright
© 2013, the Authors. Published by Atlantis Press.
Open Access
This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

<Previous Article In Volume
Next Article In Volume>
Volume Title
Proceedings of the 2nd International Conference on Computer Science and Electronics Engineering (ICCSEE 2013)
Series
Advances in Intelligent Systems Research
Publication Date
March 2013
ISBN
10.2991/iccsee.2013.237
ISSN
1951-6851
DOI
10.2991/iccsee.2013.237How to use a DOI?
Copyright
© 2013, the Authors. Published by Atlantis Press.
Open Access
This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Cite this article

risenwbib
TY  - CONF
AU  - Rui Wang
AU  - Wanwei Liu
AU  - Xiaoguang Mao
AU  - Tun Li
PY  - 2013/03
DA  - 2013/03
TI  - Incremental Semantic LTL Bounded Model Checking
BT  - Proceedings of the 2nd International Conference on Computer Science and Electronics Engineering (ICCSEE 2013)
PB  - Atlantis Press
SP  - 941
EP  - 944
SN  - 1951-6851
UR  - https://doi.org/10.2991/iccsee.2013.237
DO  - 10.2991/iccsee.2013.237
ID  - Wang2013/03
ER  -