\chapter{Continuation based C とメタ計算としての検証手法}
ソフトウェアの規模が大きくなるにつれてバグは発生しやすくなる。
バグとはソフトウェアが期待される動作以外の動作をすることである。
ここで期待された動作は仕様と呼ばれ、自然言語や論理によって記述される。
検証とは定められた環境下においてソフトウェアが仕様を満たすことを保証することである。

ソフトウェアの検証手法にはモデル検査と定理証明がある。

モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認する。
モデル検査器には Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。
定理証明を行なうことができる言語には、依存型証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。

モデル検査器や証明でソフトウェアを検証する際、検証するコードと実装に使われるコードが異なる問題がある。
検証されたコードから仕様を満たしたソースコードを生成できる機能を持つ検証系もあるが、既存の実装コードに対する検証が行なえない。
...

\section{本論文の構成}