WEKO3
-
RootNode
アイテム
証明支援系を用いたMorrisの2分木走査アルゴリズムの実装の検証
https://ipsj.ixsq.nii.ac.jp/records/107876
https://ipsj.ixsq.nii.ac.jp/records/1078767ad70289-32fc-48d9-8cdc-e2a78e7c2777
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-Z73-6L-7.pdf (216.0 kB)
|
Copyright (c) 2011 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | National Convention(1) | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2011-03-02 | |||||||||||||
| タイトル | ||||||||||||||
| タイトル | 証明支援系を用いたMorrisの2分木走査アルゴリズムの実装の検証 | |||||||||||||
| 言語 | ||||||||||||||
| 言語 | jpn | |||||||||||||
| キーワード | ||||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | ソフトウェア科学・工学 | |||||||||||||
| 資源タイプ | ||||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||||||
| 資源タイプ | conference paper | |||||||||||||
| 著者所属 | ||||||||||||||
| 東工大 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 東工大 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 東工大 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 東工大 | ||||||||||||||
| 著者名 |
山田一宏
× 山田一宏
× 森口草介
× 渡部卓雄
× 西崎真也
|
|||||||||||||
| 論文抄録 | ||||||||||||||
| 内容記述タイプ | Other | |||||||||||||
| 内容記述 | 我々は，Morrisの2分木走査アルゴリズムのCによる実装を対象として，証明支援系を用いた正当性の検証を試みた．本論文はその手法と結果に関する報告である．Morrisのアルゴリズムは，ポインタの書き換えを行うことで再帰やスタックを用いずに2分木走査を行う方法のひとつである．また他のポインタ反転法と異なり節点に印を付けるためのビットを設ける必要もないのが特徴である．我々は，入力および走査結果についての仕様を事前・事後条件として与え，C用の検証支援ツールであるCaduceusによって検証条件を生成した．ループ不変条件は必要に応じて適宜与えた．生成された検証条件を自動検証ツールSimplifyおよび証明支援系Coqを用いて証明した． | |||||||||||||
| 書誌レコードID | ||||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||||
| 収録物識別子 | AN00349328 | |||||||||||||
| 書誌情報 |
第73回全国大会講演論文集 巻 2011, 号 1, p. 505-506, 発行日 2011-03-02 |
|||||||||||||
| 出版者 | ||||||||||||||
| 言語 | ja | |||||||||||||
| 出版者 | 情報処理学会 | |||||||||||||
