Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Thu Jul 07 18:39:23 2016 +0900
+++ b/paper/vmpcbc.tex	Thu Jul 07 19:32:23 2016 +0900
@@ -51,29 +51,36 @@
 \author{河野 真治}{Shinji KONO}{RUniv}[kono@ie.u-ryukyu.ac.jp]
 
 \begin{abstract}
-Continuation based C 言語によって記述されたプログラムのデータ構造の性質を検証する手法を提案する。
-Continuation based C とは当研究室が提案している Code Segment, Data Segment という単位でプログラムを記述する言語である。
-Code Segment とは処理の単位であり、データの単位である Data Segment を入力と出力に持つ。
-プログラム全体は Code Segment どうしの接続により表現され、あるCode Segment の出力は接続された次の Code Segment の入力となる。
-また、メモリ管理やエラーの処理など、本来中心に行ないたい処理と異なる処理はメタ計算として分離し、Meta Code Segment, Meta Data Segment として記述する。
-Code Segment の接続処理を Meta Code Segment として表現し、接続部分に検証を含めることで 元の Code Segment を変更することなくプログラムの検証を行なう。
-本論文では Continuatoin based C によって記述された赤黒木といったデータ構造の性質を検証する。
+ソフトウェアが期待される仕様を満たしているか調べることは重要である。
+特に実際に動作しているソフトウェア自体を検証できると良い。
+従来はassertなどを用いて検証しているが、モデル検査のような網羅的な検査を行うことはできない。
+そこでソフトウェアの実行自体を網羅的に行うように変更する。
+これは計算自体を変更するのでメタ計算となる。
+本論文ではプログラムを Continuation based C (CbC) で記述する。
+CbC では Code Segment という単位で処理を記述する。
+CbC を用いることによりメタ計算は CbC の Code Segment 間に Meta Code Segment を挟むという単純な方法で実現できる。
+そして、通常計算との切り替えも簡単に行うことができる。
+ここでは、赤黒木を実際の例題として検証した。
+比較対象としてANSI-Cの記号実行を行うCBMC\cite{cite:cmbc}でも検証する。
+CBMCよりも広い範囲の検査が行えることを確認した。
 \end{abstract}
 
-
 \begin{jkeyword}
 プログラミング言語, 検証, 赤黒木
 \end{jkeyword}
 
 \begin{eabstract}
-We propose a verification method for executable programs using Continuation based C language.
-Our laboratory develops Continuation based C language which supports programming unit called Code Segment, Data Segment.
-Code segments are calculation units which have input/output data segments that data unit.
-Programs are represented by connections among with code segments and code segments.
-The output data segment of some code segment is converted to the input data segment of connected one.
-We introduce meta computations which split main computations and complicated computations such as memory control, error handling and more.
-Meta computations represented to meta code segment and meta data segment, which saves main computations.
-In this paper, We define a meta computation which connects code segments with verifications and verify properties of data structures such as Red-Black Tree.
+Checking desirable specifications of software is important.
+If it checks actual implementations, much better.
+Currently, assertions in the implementations is used, but it does not verify all possible executions like a model checker.
+We propose a modification of program executions to do the verification.
+This kind of modification is called a meta computation.
+In this paper, we describe programs in Continuation based C(CbC).
+CbC programs is composed of Code Segments.
+Using CbC, meta computations is easily implemented as an insertion of meta code segment between normal level code segments.
+Red-black Tree is verified by with our method.
+We also check it with CBMC which execute ANSI-C programs symbolically.
+Our method covers wider range of execution of the program.
 \end{eabstract}
 
 \begin{ekeyword}