--- a/paper/abstract.tex	Mon Feb 06 10:32:49 2017 +0900
+++ b/paper/abstract.tex	Mon Feb 06 15:42:45 2017 +0900
@@ -1,3 +1,14 @@
 \begin{abstract}
+ソフトウェアが期待される仕様を満たすか検査することは重要である。
+特に実際に動作するソフトウェアを検証できるとなお良い。
+
+本論文では Continuation based C(CbC) 言語で記述されたプログラムを検証用に変更せず信頼性を確保する手法を二つ提案する。
+一つはプログラムが持つ状態を数え挙げ、常に仕様を満たすことを保証するモデル検査的手法である。
+プログラムの実行を網羅的に行なうよう変更するメタ計算ライブラリ akasha を用いて赤黒木の仕様を検証する。
+
+もう一つの信頼性向上手法としてデータ構造の持つ性質を証明する手法を提案する。
+プログラムにおける証明は Curry-Howard Isomorphism により型付き $\lambda$計算に対応する。
+プログラムを型付けできるよう、CbC の型システムを部分型を用いて定義する。
+加えて、型の定義を用いて証明支援系言語 Agda 上で CbC のプログラムを記述し、データ構造の性質を証明する。
 
 \end{abstract}

--- a/paper/abstract_eng.tex	Mon Feb 06 10:32:49 2017 +0900
+++ b/paper/abstract_eng.tex	Mon Feb 06 15:42:45 2017 +0900
@@ -1,3 +1,13 @@
 \begin{abstract_eng}
-    
+Checking desirable specifications of software are important.
+If it checks actual implementations, much better.
+
+In this papaer, We propose two verification methods using meta computations which save original implementations.
+On the hand method verify specification by enumerate possible states on programs.
+We checked red-black tree specification using our meta computation library named Akasha, which override program executions exhaustively.
+
+On the other hand method veriy programs with proofs.
+Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism.
+We define the CbC type system with subtype for proving CbC itself.
+Agda proves properties of translated CbC programs using proposed subtype definition.
 \end{abstract_eng}

Binary file paper/atton-master.pdf has changed