Effective Predicate Abstraction for Program Verification

摘要：

The paper presents a new approach to computing the abstract state and a maximum weight heuristic method for finding the shortest counter-example in verification of imperative programs. The strategy is incorporated in a verification system based on the counterexample-guided abstraction refinement method. The proposed method slashes both the size of the abstract state space and the number of invokes of a decision procedure. A number of benchmarks are employed to evaluate the effectiveness of the approach.

作者: Li Li Ming Gu Xiaoyu Song Jianmin Wang

作者单位: Dept.Computer Science & Technology, Tsinghua University, Beijing, China Key Laboratory for Informati Key Laboratory for Information System Security, Ministry of Education China School of Software, Tsin Dept.ECE, Portland State University, Oregon, USA School of Software, Tsinghua University, Beijing, China Dept.ECE, Portland State University, Oregon,

会议类型: 国际会议

会议名称: 第二届IFIP/IEEE软件工程理论基础国际研讨会(TASE 2008)(Second IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering)

会议地点: 南京

会议语种:英文

页码: 129-132

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