| 講演名 | 2011-03-08 プログラム変換を用いたポインタ操作プログラムの検証にむけて : Morrisの二分木走査アルゴリズムによるケーススタディ 渡部 卓雄, 森口 草介, 山田 一宏, 西崎 真也, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | ポインタ書き換えを伴うプログラムのプログラム変換にもとづく検証のケーススタディとして,Morrisの二分木走査アルゴリズムの正当性を扱った.本稿ではその際に用いたプログラム変換手法とその具体的な適用手法について報告する. |
| 抄録(英) | We proved the correctness of a C implementation of Morris's tree traversal algorithm. The algorithm is known as a recursion-free, stack-free and tag-free binary tree traversal. This work is intended to be a case study of verifying C programs with pointer manipulation by using program transformation. In this report, we describe the outline of the verification methodology and results. |
| キーワード(和) | プログラム検証 / プログラム変換 / ポインタ操作 / Morrisの二分木走査アルゴリズム |
| キーワード(英) | program verification / program transformation / pointer manipulation / Morris' tree traversal algorithm |
| 資料番号 | SS2010-69 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2011/2/28(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | プログラム変換を用いたポインタ操作プログラムの検証にむけて : Morrisの二分木走査アルゴリズムによるケーススタディ |
| サブタイトル（和） | |
| タイトル（英） | Towards Verifying Pointer-Manipulating Programs using Program Transformation : A Case Study with Morris' Binary Tree Traversal Algorithm |
| サブタイトル（和） | |
| キーワード(1)（和/英） | プログラム検証 / program verification |
| キーワード(2)（和/英） | プログラム変換 / program transformation |
| キーワード(3)（和/英） | ポインタ操作 / pointer manipulation |
| キーワード(4)（和/英） | Morrisの二分木走査アルゴリズム / Morris' tree traversal algorithm |
| 第 1 著者 氏名（和/英） | 渡部 卓雄 / Takuo WATANABE |
| 第 1 著者 所属（和/英） | 東京工業大学大学院情報理工学研究科計算工学専攻 Department of Computer Science, Tokyo Institute of Technology |
| 第 2 著者 氏名（和/英） | 森口 草介 / Sosuke MORIGUCHI |
| 第 2 著者 所属（和/英） | 東京工業大学大学院情報理工学研究科計算工学専攻 Department of Computer Science, Tokyo Institute of Technology |
| 第 3 著者 氏名（和/英） | 山田 一宏 / Kazuhiro YAMADA |
| 第 3 著者 所属（和/英） | 東京工業大学大学院情報理工学研究科計算工学専攻 Department of Computer Science, Tokyo Institute of Technology |
| 第 4 著者 氏名（和/英） | 西崎 真也 / Shin-ya NISHIZAKI |
| 第 4 著者 所属（和/英） | 東京工業大学大学院情報理工学研究科計算工学専攻 Department of Computer Science, Tokyo Institute of Technology |
| 発表年月日 | 2011-03-08 |
| 資料番号 | SS2010-69 |
| 巻番号（vol） | vol.110 |
| 号番号（no） | 458 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |