--- a/paper/introduction.tex	Fri Jan 20 16:37:04 2017 +0900
+++ b/paper/introduction.tex	Sun Jan 22 16:24:59 2017 +0900
@@ -11,8 +11,21 @@
 定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。
 定理証明を行なうことができる言語には、依存型証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。
 
-モデル検査器や証明でソフトウェアを検証する際、検証するコードと実装に使われるコードが異なる問題がある。
-検証されたコードから仕様を満たしたソースコードを生成できる機能を持つ検証系もあるが、既存の実装コードに対する検証が行なえない。
-...
+モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。
+言語が異なれば二重で同じソフトウェアをせざるを得なくなる上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。
+検証されたコードから実行可能なコードを生成可能な検証系もあるが、既存の実装に対する検証は行なえない。
+そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{cbc} 言語を開発している。  %TODO: ref
+
+Continuation based C (CbC)はC言語と似た構文を持つ言語である。
+CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。
+CodeSegment は値を入力として受け取り出力を行なう処理単位であり、CodeSegment を接続していくことによりソフトウェアを構築していく。
+CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。
+検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更することなくソフトウェアの検証を行なうことができる。
+
+本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
+モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
+また、証明的な検証として CbC における型システムを部分型として定義し、それを利用してCbC のプログラムが証明支援系言語 Agda 上で正しく証明可能な形で定義できることを示す。
+
+
 
 \section{本論文の構成}