WEKO3
アイテム
Gears Agda による Red Black Tree の検証
https://ipsj.ixsq.nii.ac.jp/records/232323
https://ipsj.ixsq.nii.ac.jp/records/23232341f8dafd-bfdd-4cc1-ad78-9c35ba434158
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WPRO2022012.pdf (314.7 kB)
|
Copyright (c) 2022 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2022-01-07 | |||||||
| タイトル | ||||||||
| タイトル | Gears Agda による Red Black Tree の検証 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Red Black Tree verification by Gears Agda | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | プログラミング言語, CbC, Gears OS, Agda, 検証 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
| 資源タイプ | conference paper | |||||||
| 著者所属 | ||||||||
| 琉球大学大学院理工学研究科工学専攻知能情報プログラム | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Computer sience & Intelligent systems, University of the Ryukyus | ||||||||
| 著者名 |
上地, 悠斗
× 上地, 悠斗
|
|||||||
| 著者名(英) |
Yuto, Uechi
× Yuto, Uechi
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | OS やアプリケーションの信頼性を高めることは重要な課題である。信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。当研究室では Continuation based C (CbC) という言語を開発している。CbC とは、 C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C 言語の下位言語である。その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。検証には定理証明を用いるため、 定理証明支援器の Agda を用いる。agda が変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である red black tree の検証を行う | |||||||
| 書誌情報 |
第63回プログラミング・シンポジウム予稿集 巻 2022, p. 51-62, 発行日 2022-01-07 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
