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

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

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

\end{abstract}