\begin{abstract}
ソフトウェアが期待される仕様を満たすか検査することは重要である。
特に実際に動作するソフトウェアを検証できるとなお良い。

本論文では Continuation based C(CbC) 言語で記述されたプログラムを検証用に変更せず信頼性を確保する手法を二つ提案する。
一つはプログラムが持つ状態を数え挙げ、常に仕様を満たすことを保証するモデル検査的手法である。
プログラムの実行を網羅的に行なうよう変更するメタ計算ライブラリ akasha を用いて赤黒木の仕様を検証する。

もう一つの信頼性向上手法として、プログラムのデータ構造の性質を証明する手法を提案する。
プログラムにおける証明は Curry-Howard Isomorphism により型付き $\lambda$計算に対応している。
CbC プログラムの性質を証明できるよう、部分型を用いてCbC の型システムを定義する。
加えて、型システムの定義を用いて証明支援系言語 Agda 上に CbC のプログラムを記述し、証明を行なう。

\end{abstract}