Incremental Semantic LTL Bounded Model Checking

摘要：

　　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.

关键词： bounded model checking semantic encoding incremental NuSMV

作者: Rui Wang Wanwei Liu Xiaoguang Mao Tun Li

作者单位: School of Computer Science National University of Defense Technology Changsha,Hunan

会议类型: 国际会议

会议名称: 2013 2nd International Conference on Computer Science and Electronics Engineering(ICCSEE2013)(2013年第二届计算机科学与电子工程国际会议)

会议地点: 杭州

会议语种:英文

页码: 941-944

在线出版日期: 2013-03-22（万方平台首次上网日期，不代表论文的发表时间）