본문 바로가기
  • Home

Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification

  • Journal of The Korea Society of Computer and Information
  • Abbr : JKSCI
  • 2012, 17(8), pp.61-69
  • Publisher : The Korean Society Of Computer And Information
  • Research Area : Engineering > Computer Science

김제민 1 Seontae Kim 1 PARK JOONSEOK 1 Weon Hee Yoo 1

1인하대학교

Accredited

ABSTRACT

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.

Citation status

* References for papers published after 2022 are currently being built.