文献

J-GLOBAL ID：202202264848200888   整理番号：22A0361391

Gears AgdaによるRed Black Treeの検証

著者 (2件)： 上地悠斗 (琉球大 大学院理工学研究科) ,  河野真治 (琉球大 大学院理工学研究科)
資料名： 情報処理学会プログラミング・シンポジウム予稿集  (プログラミング・シンポジウム予稿集)
巻： 63rd  ページ： 51-62  発行年： 2022年01月31日 
JST資料番号： G0897A  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

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

シソーラス用語： *プログラム検証 ,  *プログラミング言語 ,  オペレーティングシステム ,  応用プログラム ,  信頼性 ,  モデル検査 ,  定理証明 ,  データ構造
準シソーラス用語： アプリケーション ,  OS

分類 (2件)： 計算理論  (JB02000A) ,  汎用プログラミング言語  (JD03051H)

引用文献 (27件)：

• The Agda wiki, http://wiki.portal.chalmers.se/agda/pmwiki.php. Accessed: 2021/11/29(Mon).
• Agdal, https://sourceforge.net/projects/agda/. Accessed: 2020/2/9(Sun).
• ATS-PL-SYS, http://www.ats-lang.org/. Accessed: 2020/2/9(Sun).
• cbc-gcc-並列信頼研 mercurial repository, http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/. Accessed: 2021/11/28(Sun).
• cbc-llvm-並列信頼研 mercurial repository, http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/. Accessed: 2021/11/28(Sun).

タイトルに関連する用語 (1件)： 検証