DocumentCode
1943119
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
fYear
2008
fDate
17-19 June 2008
Firstpage
129
Lastpage
132
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/TASE.2008.18
Filename
4549897
Link To Document