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. |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论