2026-05-20T17:20:46Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00218155 2025-01-19T15:14:56Z 1164:1867:10898:10929

Gears Agda上のモデル検査の形式化 上地, 悠斗 河野, 真治 言語・ランタイム 当研究室では Continuation based C（CbC）という言語を用いて，拡張性と信頼性を両立する OS である Gears OS を開発している．CbC とは，C 言語から通常の関数呼び出しではなく，アセンブラでいう jmp 命令により関数を遷移する継続を導入した C 言語の下位言語である．すでに Gears OS はメタ計算によるモデル検査機構を持っている．GearsOS の CodeGear/DataGearはGears Agda により形式証明に向いた形に記述することができる．モデル検査機構を Gears Agda により記述することで Hoare Logic 的な逐次実行型のプログラムの証明だけでなく，並行実行を含むプログラムの証明が可能になる． technical report 情報処理学会 2022-05-19 application/pdf 研究報告システムソフトウェアとオペレーティング・システム（OS） 13 2022-OS-155 1 5 2188-8795 AN10444176 https://ipsj.ixsq.nii.ac.jp/record/218155/files/IPSJ-OS22155013.pdf jpn