loading...
Effective Predicate Abstraction for Program Verification
June 17-June 19
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2008.182008 2nd IFIP/IEEE International Symp ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Li Li, Ming Gu, Xiaoyu Song, Jianmin Wang, "Effective Predicate Abstraction for Program Verification," Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on, pp. 129-132, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008.
 
 
BibTex
x
 
@article{ 10.1109/TASE.2008.18,
author = {Li Li and Ming Gu and Xiaoyu Song and Jianmin Wang},
title = {Effective Predicate Abstraction for Program Verification},
journal ={Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on},
volume = {0},
year = {2008},
isbn = {978-0-7695-3249-3},
pages = {129-132},
doi = {http://doi.ieeecomputersociety.org/10.1109/TASE.2008.18},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on
TI - Effective Predicate Abstraction for Program Verification
SN - 978-0-7695-3249-3
SP129
EP132
A1 - Li Li,
A1 - Ming Gu,
A1 - Xiaoyu Song,
A1 - Jianmin Wang,
PY - 2008
KW - program verification
KW - predicate abstraction
VL - 0
JA - Theoretical Aspects of Software Engineering, Joint IEEE/IFIP Symposium on
ER -
 
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 counter example-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.
Index Terms:
program verification, predicate abstraction
Citation:
Li Li, Ming Gu, Xiaoyu Song, Jianmin Wang, "Effective Predicate Abstraction for Program Verification," tase, pp.129-132, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008
Usage of this product signifies your acceptance of the Terms of Use.