# HG changeset patch # User Yasutaka Higa # Date 1481443765 -32400 # Node ID 1f2ee43be9d0ab74bf765a873bfdb77c0582d9b2 # Parent c73e1ee2d5ee57244d47d48ec1c8167710da0340 Fix english abstract diff -r c73e1ee2d5ee -r 1f2ee43be9d0 abstract/abst5_higa.tex --- 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