# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1467609014 -32400
# Node ID aab1f02f16e867ff802ba78dc83d2ed3c5a61c27
# Parent  784913eb2902e35a3a4af779539afd94d3bd689e
Wrote section 4

diff -r 784913eb2902 -r aab1f02f16e8 paper/vmpcbc.tex
--- a/paper/vmpcbc.tex	Mon Jul 04 13:59:34 2016 +0900
+++ b/paper/vmpcbc.tex	Mon Jul 04 14:10:14 2016 +0900
@@ -143,9 +143,14 @@
 cbmcで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。
 
 \section{まとめと今後の課題}
-% unbounded にする
-% 状態の抽象化
-% 証明を使った空間削減
+コードセグメントとデータセグメントを用いたプログラミング手法を用いる言語CbCで記述したプログラムに対する仕様の検証を行なうことができた。
+メタ計算として検証を行なうことで、実際に動作するプログラムを全く変更することなくプログラムを検証した。
+
+今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
+本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。
+木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。
+また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。
+さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。
 
 \begin{thebibliography}{9}
 \bibitem{okumura}