국립중앙도서관 "우편 복사 서비스"로 연결 됩니다.
ScienceON
DBpiaBIRS 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 ...
다국어 입력
あ
ぁ
か
が
さ
ざ
た
だ
な
は
ば
ぱ
ま
や
ゃ
ら
わ
ゎ
ん
い
ぃ
き
ぎ
し
じ
ち
ぢ
に
ひ
び
ぴ
み
り
う
ぅ
く
ぐ
す
ず
つ
づ
っ
ぬ
ふ
ぶ
ぷ
む
ゆ
ゅ
る
え
ぇ
け
げ
せ
ぜ
て
で
ね
へ
べ
ぺ
め
れ
お
ぉ
こ
ご
そ
ぞ
と
ど
の
ほ
ぼ
ぽ
も
よ
ょ
ろ
を
ア
ァ
カ
サ
ザ
タ
ダ
ナ
ハ
バ
パ
マ
ヤ
ャ
ラ
ワ
ヮ
ン
イ
ィ
キ
ギ
シ
ジ
チ
ヂ
ニ
ヒ
ビ
ピ
ミ
リ
ウ
ゥ
ク
グ
ス
ズ
ツ
ヅ
ッ
ヌ
フ
ブ
プ
ム
ユ
ュ
ル
エ
ェ
ケ
ゲ
セ
ゼ
テ
デ
ヘ
ベ
ペ
メ
レ
オ
ォ
コ
ゴ
ソ
ゾ
ト
ド
ノ
ホ
ボ
ポ
モ
ヨ
ョ
ロ
ヲ
―
http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
예시)
- 中文 을 입력하시려면 zhongwen을 입력하시고 space를누르시면됩니다.
- 北京 을 입력하시려면 beijing을 입력하시고 space를 누르시면 됩니다.
А
Б
В
Г
Д
Е
Ё
Ж
З
И
Й
К
Л
М
Н
О
П
Р
С
Т
У
Ф
Х
Ц
Ч
Ш
Щ
Ъ
Ы
Ь
Э
Ю
Я
а
б
в
г
д
е
ё
ж
з
и
й
к
л
м
н
о
п
р
с
т
у
ф
х
ц
ч
ш
щ
ъ
ы
ь
э
ю
я
′
″
℃
Å
￠
￡
￥
¤
℉
‰
＄
％
Ｆ
￦
㎕
㎖
㎗
ℓ
㎘
㏄
㎣
㎤
㎥
㎦
㎙
㎚
㎛
㎜
㎝
㎞
㎟
㎠
㎡
㎢
㏊
㎍
㎎
㎏
㏏
㎈
㎉
㏈
㎧
㎨
㎰
㎱
㎲
㎳
㎴
㎵
㎶
㎷
㎸
㎹
㎀
㎁
㎂
㎃
㎄
㎺
㎻
㎽
㎾
㎿
㎐
㎑
㎒
㎓
㎔
Ω
㏀
㏁
㎊
㎋
㎌
㏖
㏅
㎭
㎮
㎯
㏛
㎩
㎪
㎫
㎬
㏝
㏐
㏓
㏃
㏉
㏜
㏆
https://www.riss.kr/link?id=A101700113
- 저자
- 발행기관
- 학술지명
- 권호사항
-
발행연도
2012
-
작성언어
Korean
- 주제어
-
KDC
004
-
등재정보
KCI등재
-
자료형태
학술저널
- 발행기관 URL
-
수록면
61-69(9쪽)
-
KCI 피인용횟수
0
- DOI식별코드
- 제공처
-
0
상세조회 -
0
다운로드
부가정보
다국어 초록 (Multilingual 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.
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.
참고문헌 (Reference)
1 김선태, "자바 프로그램 검증을 위한 스택 리스 중간 표현 언어 생성기 구현" 한국정보기술학회 9 (9): 129-138, 2011
2 김제민, "자바 바이트코드의 검증을 위한 프레임워크 설계" (사)디지털산업정보학회 7 (7): 29-37, 2011
3 김지민, "바이트코드를 위한 정적 단일 배정문 기반의 정적 타입 추론" 한국컴퓨터정보학회 11 (11): 87-96, 2006
4 김경수, "바이트코드 분석을 위한 중간코드에 관한 연구" 한국컴퓨터정보학회 11 (11): 107-118, 2006
5 M. Barnett, "Weakest-precondition of unstructured programs" 82-87, 2005
6 Mike Barnett, "The Spec# Programming System : An Overview" 3362 : 2004
7 David Detlefs, "Simplify : a theorem prover for programchecking" 52 (52): 365-473, 2005
8 Lilian Burdy, "Preliminary Design of BML : A Behavioral Interface Specification Language for Java bytecode" 4422 : 215-229, 2007
9 Z. Manna, "Mathematical Theory of Computation" Dover Publications 2003
10 Gilles Barthe, "JACK : a tool for validation of security and behaviour of Java applications" 152-174, 2007
1 김선태, "자바 프로그램 검증을 위한 스택 리스 중간 표현 언어 생성기 구현" 한국정보기술학회 9 (9): 129-138, 2011
2 김제민, "자바 바이트코드의 검증을 위한 프레임워크 설계" (사)디지털산업정보학회 7 (7): 29-37, 2011
3 김지민, "바이트코드를 위한 정적 단일 배정문 기반의 정적 타입 추론" 한국컴퓨터정보학회 11 (11): 87-96, 2006
4 김경수, "바이트코드 분석을 위한 중간코드에 관한 연구" 한국컴퓨터정보학회 11 (11): 107-118, 2006
5 M. Barnett, "Weakest-precondition of unstructured programs" 82-87, 2005
6 Mike Barnett, "The Spec# Programming System : An Overview" 3362 : 2004
7 David Detlefs, "Simplify : a theorem prover for programchecking" 52 (52): 365-473, 2005
8 Lilian Burdy, "Preliminary Design of BML : A Behavioral Interface Specification Language for Java bytecode" 4422 : 215-229, 2007
9 Z. Manna, "Mathematical Theory of Computation" Dover Publications 2003
10 Gilles Barthe, "JACK : a tool for validation of security and behaviour of Java applications" 152-174, 2007
11 John Barnes, "High Integrity Software: The SPARK Approach to Safety and Security" Addison Wesley 2005
12 H. Lehner, "Formal translation of bytecode into BoogiePL" 190 (190): 35-50, 2007
13 Cormac Flanagan, "Extended static checking for Java" 37 (37): 234-245, 2002
14 "Eiffel Software"
15 J. M. Jazequel, "Design by contract : the lessons of Ariane" 30 (30): 129-130, 1997
16 C. Flanagan, "Avoiding exponential explosion : generating compact verification conditions" 36 (36): 193-205, 2001
17 R. W. Floyd, "Assigning meaning to programs" 19 : 19-32, 1967
18 Lilian Burdy, "An overview of JML tools and applications" 7 (7): 212-232, 2005
19 C. A. R. Hoare, "An axiomatic basis for computer programming" 12 (12): 576-580, 1969
20 E. W. Dijkstra, "A Discipline of Programming" Prentice Hall 1976
동일학술지(권/호) 다른 논문
-
- 한국컴퓨터정보학회
- 장석우(Seok-Woo Jang)
- 2012
- KCI등재
-
GPS-CDMA 모뎀 일체 단말기 및 LBS 기반 자전거 관제 시스템 개발
- 한국컴퓨터정보학회
- 이형봉(Hyung-Bong Lee)
- 2012
- KCI등재
-
모의실험을 통한 역 RZ 부호로 코딩된 하향신호의 재변조를 이용한 5Gbps/1.25Gbps WDM/TDM 하이브리드 수동 광가입자 망의 성능분석
- 한국컴퓨터정보학회
- 박상조(Sang-Jo Park)
- 2012
- KCI등재
-
클라우드 컴퓨팅에서의 의미 상호운용성을 위한 표준 참조 모델
- 한국컴퓨터정보학회
- 정동원(Dong-Won Jeong)
- 2012
- KCI등재
분석정보
인용정보 인용지수 설명보기
학술지 이력
| 연월일 | 이력구분 | 이력상세 | 등재구분 |
|---|---|---|---|
| 2026 | 평가 | 재인증평가 신청대상 (재인증) | |
| 2020-01-01 | 등재 | 등재학술지 유지 (재인증) |  |
| 2017-01-01 | 등재 | 등재학술지 유지 (계속평가) | |
| 2013-01-01 | 등재 | 등재학술지 유지 (등재유지) | |
| 2010-01-01 | 등재 | 등재학술지 유지 (등재유지) | |
| 2007-01-01 | 등재 | 등재학술지 선정 (등재후보2차) | |
| 2006-01-01 | 등재 | 등재후보 1차 PASS (등재후보1차) |  |
| 2004-07-01 | 등재 | 등재후보학술지 선정 (신규평가) | |
학술지 인용정보
| 기준연도 | WOS-KCI 통합IF(2년) | KCIF(2년) | KCIF(3년) |
|---|---|---|---|
| 2016 | 0.44 | 0.44 | 0.44 |
| KCIF(4년) | KCIF(5년) | 중심성지수(3년) | 즉시성지수 |
| 0.43 | 0.38 | 0.58 | 0.15 |
이 자료와 함께 이용한 RISS 자료
나만을 위한 추천자료
