@techreport{oai:ipsj.ixsq.nii.ac.jp:00218155,
 author = {上地, 悠斗 and 河野, 真治},
 issue = {13},
 month = {May},
 note = {当研究室では Continuation based C（CbC）という言語を用いて，拡張性と信頼性を両立する OS である Gears OS を開発している．CbC とは，C 言語から通常の関数呼び出しではなく，アセンブラでいう jmp 命令により関数を遷移する継続を導入した C 言語の下位言語である．すでに Gears OS はメタ計算によるモデル検査機構を持っている．GearsOS の CodeGear/DataGearはGears Agda により形式証明に向いた形に記述することができる．モデル検査機構を Gears Agda により記述することで Hoare Logic 的な逐次実行型のプログラムの証明だけでなく，並行実行を含むプログラムの証明が可能になる．},
 title = {Gears Agda上のモデル検査の形式化},
 year = {2022}
}