Title :
Effective Predicate Abstraction for Program Verification
Author :
Li, Li ; Gu, Ming ; Song, Xiaoyu ; Wang, Jianmin
Author_Institution :
Dept. Comput. Sci. & Technol., Tsinghua Univ., Beijing
Abstract :
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.
Keywords :
program verification; counterexample-guided abstraction refinement method; maximum weight heuristic method; predicate abstraction; program verification; Computer science; Computer science education; Computer security; Concrete; Educational technology; Information security; Information systems; Laboratories; Software engineering; State-space methods; predicate abstraction; program verification;
Conference_Titel :
Theoretical Aspects of Software Engineering, 2008. TASE '08. 2nd IFIP/IEEE International Symposium on
Conference_Location :
Nanjing
Print_ISBN :
978-0-7695-3249-3
DOI :
10.1109/TASE.2008.18
