loading...
Verifying Java Programs By Theorem Prover HOL
Chicago, Illinois September 17-September 21
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/COMPSAC.2006.8530th Annual International Computer So ...
 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 
 
Anduo Wang, He Fei, Ming Gu, Xiaoyu Song, "Verifying Java Programs By Theorem Prover HOL," Computer Software and Applications Conference, Annual International, vol. 1, pp. 139-142, 30th Annual International Computer Software and Applications Conference (COMPSAC'06), 2006.
 
 
BibTex
x
 
@article{ 10.1109/COMPSAC.2006.85,
author = {Anduo Wang and He Fei and Ming Gu and Xiaoyu Song},
title = {Verifying Java Programs By Theorem Prover HOL},
journal ={Computer Software and Applications Conference, Annual International},
volume = {1},
year = {2006},
issn = {0730-3157},
pages = {139-142},
doi = {http://doi.ieeecomputersociety.org/10.1109/COMPSAC.2006.85},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Software and Applications Conference, Annual International
TI - Verifying Java Programs By Theorem Prover HOL
SN - 0730-3157
SP139
EP142
A1 - Anduo Wang,
A1 - He Fei,
A1 - Ming Gu,
A1 - Xiaoyu Song,
PY - 2006
KW - null
VL - 1
JA - Computer Software and Applications Conference, Annual International
ER -
 
Anduo Wang, Tsinghua University, China
He Fei, Tsinghua University, China
Ming Gu, Tsinghua University, China
Xiaoyu Song, Portland State University, USA
Program verification plays an important role in assuring the reliability of software systems. This paper presents a novel verification methodology for Java programs based on the higher-order logic theorem proving system HOL. The soundness of a Java program in accordance with its specification in annotation is established in HOL4. A Hoare-logic based verification methodology (WHY) guides the verification process. As a case study, a Java program with four methods is specified in JML annotation and proved in HOL. The flexible manipulation of pure method call in annotation is presented in the HOL proof mechanism. This work may constitute the first attempt on using the proving system HOL for Java programs. The experience demonstrates the effectiveness and the promising results of the approach.
Citation:
Anduo Wang, He Fei, Ming Gu, Xiaoyu Song, "Verifying Java Programs By Theorem Prover HOL," compsac, vol. 1, pp.139-142, 30th Annual International Computer Software and Applications Conference (COMPSAC'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions