--- a/paper/vmpcbc.tex	Wed Jul 06 14:26:44 2016 +0900
+++ b/paper/vmpcbc.tex	Wed Jul 06 14:27:50 2016 +0900
@@ -41,19 +41,11 @@
 \begin{document}
 
 % ipsjpro
-%     研究背景とか
-%         nusmv, spin
 %     llrb の実装を書いても良い
 %         stack の話とか
 %     どうやって akasha で検証しているか
 %     cbmc でできなかった理由とかも書く
 %         実際はフェアじゃないし
-%         あと cbmc じゃなくて CBMC かな
-% しゅうろん
-%     operational semantics
-%     akashaをもうちょい綺麗に
-%     cbc を綺麗に
-%         python code周りとか
 %
 % --- たけだくんから ---
 % Attonさん
@@ -76,7 +68,6 @@
 % CBCで書かれたRed black Treeも書いた方がいい
 %
 % 検証できる範囲を検証できなかったというのはおかしい
-% cbmcは大文字
 %
 % うりとしては実コードで検証できる
 % 挿入する要素数がある程度あれば
@@ -315,7 +306,7 @@
 Code\ref{src:specification}で定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。
 
-当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc\cite{cite:cbmc} を用いてこの仕様を検証した。
+当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いてこの仕様を検証した。
 akasha では検証用の仕様と検証用の処理をMeta Code Segmentに定義する。
 挿入順の数え上げには深さ優先探索を用いる。
 CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するMeta Data Segmentを自ら用意する。
@@ -323,24 +314,24 @@
 要素数13個までは任意の順で挿入を行なっても仕様が満たされることをakasha を用いて検証した。
 また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。
 
-同じ仕様をC言語の有限モデルチェッカcbmcで検証する。
+同じ仕様をC言語の有限モデルチェッカCBMCで検証する。
 CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。
-CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証を行なった。
-cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることが可能である。
+CbCで記述された赤黒木のコードを置換でC言語に変換し、CBMCで検証を行なった。
+CBMC における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることが可能である。
 また、ポインタへの不正アクセスといった一般的なバグへの検証コードが機能として存在する。
-挿入順の数え上げにはcbmcの機能に存在する非決定的な入力を用いた。
-しかし、cbmcで検証できる範囲内ではGearsの赤黒木の仕様を検証することはできなかった。
+挿入順の数え上げにはCBMCの機能に存在する非決定的な入力を用いた。
+しかし、CBMCで検証できる範囲内ではGearsの赤黒木の仕様を検証することはできなかった。
 有限モデルチェッカでは探索する状態空間を指定し、それを越える範囲は探索しない。
-cbmcで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。
+CBMCで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。
 
-よって、cbmcでは検証できない範囲の検証をakashaで行なうことが確認できた。
+よって、CBMCでは検証できない範囲の検証をakashaで行なうことが確認できた。
 
 \section{まとめと今後の課題}
 CbC で記述したプログラムに対する仕様の検証を行なうことができた。
 CbC はCode SegmentとData Segmentを用いてプログラミングするため、検証用にコードを変更することなくメタ計算の切り替えで検証を行なうことができた。
 
 今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
-cbmcではポインタへの不正アクセスを行なう実行例を検出することができる。
+CBMCではポインタへの不正アクセスを行なう実行例を検出することができる。
 akashaでも一般的なエラーに対するメタ計算などを定義したい。
 本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。
 木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。