論文タイトル：Gears Agda による Red Black Tree の検証

論文タイトル英語：Red Black Tree verification by Gears Agda

キーワード：プログラミング言語, CbC, Gears OS, Agda, 検証

著者名：上地 悠斗

著者名英語：Yuto Uechi

著者所属：琉球大学大学院理工学研究科工学専攻知能情報プログラム

著者所属英語：Graduate School of Computer sience & Intelligent systems, University of the Ryukyus

論文抄録（日本語論文の場合）：OS やアプリケーションの信頼性を高めることは重要な課題である。
信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。
具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。
当研究室では Continuation based C (CbC) という言語を開発している。
CbC とは、 C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C 言語の下位言語である。
その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。検証には定理証明を用いるため、 定理証明支援器の Agda を用いる。
agda が変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である red black tree の検証を行う