\begin{thebibliography}{10}

\bibitem{cbc-gcc}
cbc-gcc - 並列信頼研 mercurial repository.
\newblock \url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}.
\newblock Accessed: 2020/2/9(Sun).

\bibitem{agda}
Ulf Norell.
\newblock Dependently typed programming in agda.
\newblock In {\em Proceedings of the 4th International Workshop on Types in
  Language Design and Implementation}, TLDI '09, pp. 1--2, New York, NY, USA,
  2009. ACM.

\bibitem{ryokka-sigos}
政尊外間, 真治河野.
\newblock Gearsosのagdaによる記述と検証.
\newblock Technical Report~5, 琉球大学大学院理工学研究科情報工学専攻,
  琉球大学工学部情報工学科, may 2018.

\bibitem{EdmundM}
{Edmund M. Clarke, Jr}.
\newblock In {\em {Model Checking, Second Edition}}, 2018.

\bibitem{ikkun-master}
東恩納琢偉.
\newblock Gears os でモデル検査を実現する方法について.
\newblock Master's thesis, 琉球大学 大学院理工学研究科 情報工学専攻, 2021.

\bibitem{kaito-lola}
Tokumori Kaito and Kono Shinji.
\newblock Implementing continuation based language in llvm and clang.
\newblock {\em LOLA 2015, Kyoto}, July 2015.

\bibitem{agda-wiki}
The agda wiki.
\newblock \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}.

\bibitem{Stump:2016:VFP:2841316}
Aaron Stump.
\newblock {\em Verified Functional Programming in Agda}.
\newblock Association for Computing Machinery and Morgan \&\#38; Claypool, New
  York, NY, USA, 2016.

\bibitem{agda-stdlib}
agda-stdlib.
\newblock \url{https://github.com/agda/agda-stdlib }.
\newblock Accessed: 2023/2/1(Wed).

\bibitem{atton-master}
比嘉健太.
\newblock メタ計算を用いた continuation based c の検証手法.
\newblock Master's thesis, 琉球大学 大学院理工学研究科 情報工学専攻, 2017.

\bibitem{agda2-hoare}
Hoare logic in agda2.
\newblock \url{https://github.com/IKEGAMIDaisuke/HoareLogic}.
\newblock Accessed: 2020/2/9(Sun).

\bibitem{cr-ryukyu}
Hoare logic - 並列信頼研 mercurial repository.
\newblock \url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/}.
\newblock Accessed: 2020/2/9(Sun).

\bibitem{hoare}
C.~A.~R. Hoare.
\newblock An axiomatic basis for computer programming.
\newblock {\em Commun. ACM}, Vol.~12, No.~10, p. 576^^e2^^80^^93580, October
  1969.

\bibitem{rbtree}
渡邉.
\newblock データ構造と基本アルゴリズム, 2000.

\bibitem{parusu-master}
伊波立樹.
\newblock Gears os の並列処理.
\newblock Master's thesis, 琉球大学 大学院理工学研究科 情報工学専攻, 2018.

\bibitem{spin}
Spin - formal verification.
\newblock \url{http://spinroot.com/}.
\newblock Accessed: 2023/2/1(Wed).

\bibitem{mitsuki-prosym}
宮城光希, 河野真治.
\newblock Codegear と datagear を持つ gears os の設計.
\newblock  第59回プログラミング・シンポジウム予稿集, 第2018巻, pp. 197--206,
  jan 2018.

\bibitem{model}
広瀬健.
\newblock コンピュータ基礎理論ハンドブック 形式的モデルと意味論, 1994.

\end{thebibliography}