Mercurial > hg > Papers > 2016 > atton-ipsjpro
changeset 15:aab1f02f16e8
Wrote section 4
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 04 Jul 2016 14:10:14 +0900 |
parents | 784913eb2902 |
children | 92136f674989 |
files | paper/vmpcbc.tex |
diffstat | 1 files changed, 8 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- 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}