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/).
Cite this article
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 -