@article{ART001689083},
author={김제민 and Seontae Kim and PARK JOONSEOK and Weon Hee Yoo},
title={Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification},
journal={Journal of The Korea Society of Computer and Information},
issn={1598-849X},
year={2012},
volume={17},
number={8},
pages={61-69},
doi={}
TY - JOUR
AU - 김제민
AU - Seontae Kim
AU - PARK JOONSEOK
AU - Weon Hee Yoo
TI - Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification
JO - Journal of The Korea Society of Computer and Information
PY - 2012
VL - 17
IS - 8
PB - The Korean Society Of Computer And Information
SP - 61
EP - 69
SN - 1598-849X
AB - BIRS is an intermediate representation for verifying Java program. Java program in the form of bytecode could be translated into BIRS code. Verification conditions are generated from the BIRS code to verify the program. We propose a method generating verification conditions for BIRS code. Generating verification conditions is composed of constructing control flow graph for BIRS code, depth first searching for the control flow graph to generate basic paths, and calculating weakest preconditions of the basic paths.
KW - BIRS;Verification conditions;Weakest preconditions
DO -
ER -
김제민, Seontae Kim, PARK JOONSEOK and Weon Hee Yoo. (2012). Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification. Journal of The Korea Society of Computer and Information, 17(8), 61-69.
김제민, Seontae Kim, PARK JOONSEOK and Weon Hee Yoo. 2012, "Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification", Journal of The Korea Society of Computer and Information, vol.17, no.8 pp.61-69. Available from: doi:
김제민, Seontae Kim, PARK JOONSEOK, Weon Hee Yoo "Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification" Journal of The Korea Society of Computer and Information 17.8 pp.61-69 (2012) : 61.
김제민, Seontae Kim, PARK JOONSEOK, Weon Hee Yoo. Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification. 2012; 17(8), 61-69. Available from: doi:
김제민, Seontae Kim, PARK JOONSEOK and Weon Hee Yoo. "Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification" Journal of The Korea Society of Computer and Information 17, no.8 (2012) : 61-69.doi:
김제민; Seontae Kim; PARK JOONSEOK; Weon Hee Yoo. Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification. Journal of The Korea Society of Computer and Information, 17(8), 61-69. doi:
김제민; Seontae Kim; PARK JOONSEOK; Weon Hee Yoo. Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification. Journal of The Korea Society of Computer and Information. 2012; 17(8) 61-69. doi:
김제민, Seontae Kim, PARK JOONSEOK, Weon Hee Yoo. Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification. 2012; 17(8), 61-69. Available from: doi:
김제민, Seontae Kim, PARK JOONSEOK and Weon Hee Yoo. "Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification" Journal of The Korea Society of Computer and Information 17, no.8 (2012) : 61-69.doi:
