|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
30th Annual International Computer Software and Applications Conference (COMPSAC'06)
Verifying Java Programs By Theorem Prover HOL
Chicago, Illinois
September 17-September 21
ISBN: 0-7695-2655-1
| ASCII Text | x | ||
| Anduo Wang, He Fei, Ming Gu, Xiaoyu Song, "Verifying Java Programs By Theorem Prover HOL," 2012 IEEE 36th Annual Computer Software and Applications Conference, 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 ={2012 IEEE 36th Annual Computer Software and Applications Conference}, 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 - 2012 IEEE 36th Annual Computer Software and Applications Conference 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 - 2012 IEEE 36th Annual Computer Software and Applications Conference ER - | |||
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.