Competent predicate abstraction in model checking  

作　　者：LI Li SONG XiaoYu GU Ming LUO XiangYu 

机构地区：[1]Department of Computer Science & Technology, Tsinghua University, Beijing 100084, China [2]Key Laboratory for Information System Security, Ministry of Education of China, Beijing 100084, China [3]School of Software, Tsinghua University, Beijing 100084, China [4]Department of ECE, Portland State University, Portland, Oregon 97207, USA

出　　处：《Science China(Information Sciences)》2011年第2期258-267,共10页中国科学（信息科学）（英文版）

基　　金：supported by the National Basic Research Program of China (Grant No. 2004CB719406);the National Natural Science Foundation of China (Grant Nos. 60635020, 90718039, 60763004)

摘　　要：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 ewluate the effectiveness of the approach.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 ewluate the effectiveness of the approach.

关 键 词：PROGRAM model checking predicate abstraction weight heuristic 

分 类 号：TP13[自动化与计算机技术—控制理论与控制工程] TN915.04[自动化与计算机技术—控制科学与工程]