Competent predicate abstraction in model checking

作     者：LI Li1,2,3, SONG XiaoYu4, GU Ming2,3 & LUO XiangYu2,3 1Department of Computer Science & Technology, Tsinghua University, Beijing 100084, China 2Key Laboratory for Information System Security, Ministry of Education of China, Beijing 100084, China 3School of Software, Tsinghua University, Beijing 100084, China 4Department of ECE, Portland State University, Portland, Oregon 97207, USA 

作者机构：1. Department of Computer Science & Technology Tsinghua University Beijing 100084 China2. Key Laboratory for Information System Security Ministry of Education of China Beijing 100084 China3. School of Software Tsinghua University Beijing 100084 China4. Department of ECE Portland State University Portland Oregon 97207 USA 

出 版 物：《Science China(Information Sciences)》 (中国科学:信息科学(英文版))

年 卷 期：2011年第54卷第2期

页      面：258-267页

核心收录：

学科分类：081203[工学-计算机应用技术] 08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：program model checking predicate abstraction weight heuristic 

摘      要：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.