QQ客服 官方微博 反馈留言

	Implication-based approximating bounded model checking
	Chen, Zhenyu ; Tao, Zhihong ; Xu, Baowen ; Wang, Lifu
	2007
英文摘要	This paper presents an iterative framework based on overapproximation and under-approximation for traditional bounded model checking (BMC). A novel feature of our approach is the approximations are defined based on 'implication' instead of 'simulation'. As a common partial order relation of logic formulas, implication is suitable for the satisfiability checking of BMC for debugging. Our approach could generate the implication-based approximations efficiently with necessary accuracy, thus it potentially enables BMC to go deeper and the output counterexamples with fewer variables are easier to understand. An experiment on a suite of Petri nets shows the effectiveness of implication-based approximating BMC. ? Springer-Verlag Berlin Heidelberg 2007.; EI; 0
语种	英语
内容类型	其他
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/411296]
专题	软件与微电子学院
推荐引用方式 GB/T 7714	Chen, Zhenyu,Tao, Zhihong,Xu, Baowen,et al. Implication-based approximating bounded model checking. 2007-01-01.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。