Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Tue Jul 05 17:54:23 2016 +0900
+++ b/paper/vmpcbc.tex	Wed Jul 06 14:26:44 2016 +0900
@@ -40,6 +40,66 @@
 
 \begin{document}
 
+% ipsjpro
+%     研究背景とか
+%         nusmv, spin
+%     llrb の実装を書いても良い
+%         stack の話とか
+%     どうやって akasha で検証しているか
+%     cbmc でできなかった理由とかも書く
+%         実際はフェアじゃないし
+%         あと cbmc じゃなくて CBMC かな
+% しゅうろん
+%     operational semantics
+%     akashaをもうちょい綺麗に
+%     cbc を綺麗に
+%         python code周りとか
+%
+% --- たけだくんから ---
+% Attonさん
+%
+% オブジェクトレベルがないとのだれも論文はわからない
+% meta levelの話がいきなり来ている
+% stub
+%
+% どれがメタでどれがオブジェクトがちゃんと書いたほうがいい
+%
+% メタとstubの関係
+% 今のred black treeがあんまり綺麗に書かれてないのがそもそも問題
+% sm
+% new smvとかちゃんと知ってますよと書いたほうがいいかも・・・
+%
+% 同じようなことをやってる人の論文を見るといいかも
+% 背景などもわかるかも
+%
+% Treeの大きさがどれくらいなのかという図
+% CBCで書かれたRed black Treeも書いた方がいい
+%
+% 検証できる範囲を検証できなかったというのはおかしい
+% cbmcは大文字
+%
+% うりとしては実コードで検証できる
+% 挿入する要素数がある程度あれば
+%
+% Treeeをランダムに生成する
+%
+% なぜswitchを入れている？
+% セグフォした時に前のコードがわからない
+% ー＞デバッグ用のコード
+%
+% 次のためにみたいなので
+% const struct Node* node = akashaInfo -> akashaNode-> Node;の go toの部分
+%
+% red black treeで2ページぐらいでスタックの部分ももりもり書いてもいい
+%
+% なぜcbcで苦労して書くのか？
+% toy program的なのを書きたい
+%
+% パルスさんの書いたコンピテーション部分を持ってく
+% kkbさんの修論があればいいなぁ
+%
+% ポインターの計算とかはAkashaにはない
+% cbmcであればこういう風に書けば検証できる
 
 \title{Continuation based C を用いたプログラムの検証手法}
 \etitle{Verification method of programs using Continuation based C}
@@ -85,14 +145,20 @@
 
 \maketitle
 
-\section{Code SegmentとData Segment}
+\section{ソフトウェアの検証}
+ソフトウェアの規模が大きくなるにつれ、バグは発生しやすくなる。
+バグとはソフトウェアが期待される動作とは異なる動作を行なうことである。
+また、ソフトウェアの期待される動作を定義したものは仕様と呼ばれ、自然言語や論理で記述される。
+検証とは、ソフトウェアが定められた環境下において仕様を満たすことを保証するものである。
+ソフトウェアが仕様を満たすことを保証する手法として、定理証明とモデル検査がある。
+定理証明はプログラムが満たすべき仕様を論理式で記述し、その式が常に真であることを証明する。
+定理証明を行なう言語には Agda\cite{cite:agda} や Coq\cite{cite:coq} などが存在する。
+モデル検査を行なうモデル検査器には、 promela と呼ばれる言語でモデルを記述する spin\cite{cite:spin} やモデルを状態遷移系で記述する NuSMV\cite{cite:nusmv} 、C言語を記号実行することができる CBMC\cite{cite:cbmc} などが存在する。
+証明やモデル検査器で検証を行なう際、実際に動作するコードでなく証明用にコードを書き直す必要があるなど、実際の実装との乖離が存在する。
+よって、検証した環境では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
-プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。
-プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法\cite{cite:agda}やプログラムの状態を全て数えあげるモデルチェッカ\cite{cite:cbmc}などが存在する。
-しかし、証明では実際に動作するコードでなく証明用にコードを書き直したり、モデルチェッカでは高速化のために抽象化した記号実行によって性質が検証されるなど、実際に動作するコードとの乖離が発生してしまう。
-よって、検証した環境では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
-仕様とその実装コードの信頼性を保証するため、実際に動作するコードの検証を行なう。
 
+\section{Code SegmentとData Segment}
 動作するコードを検証しやすいよう、本研究室ではCode SegmentとData Segmentを用いるプログラミングスタイルを提案している。
 Code Segmentとは処理の単位であり、ループを含まない単純な処理のみを行なう。
 プログラムはCode Segmentどうしを組み合わせることで構築される(図\ref{fig:csds})。