--- a/abstract/abst5_higa.tex	Sun Dec 11 16:55:59 2016 +0900
+++ b/abstract/abst5_higa.tex	Sun Dec 11 17:09:25 2016 +0900
@@ -42,18 +42,18 @@
 \end{abstract}
 
 \begin{eabstract}
-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 study, 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.
+Checking desirable specifications of software are important.
+If it checks actual implementations, much better.
+Currently, assertions in the implementations are 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 study, we describe programs in Continuation based C(CbC).
+CbC programs are composed of Code Segments.
+Using CbC, meta computations are easily implemented as an insertion of meta code segment between normal level code segments.
+Red-black Tree is verified by our method.
+We also check it with CBMC which executes ANSI-C programs symbolically.
+Our method covers wider a range of execution of the program.
+
 \end{eabstract}
 
 \maketitle