\documentclass[PRO,abstract,submit]{ipsj}

\setcounter{巻数}{10}
\setcounter{号数}{1}
\setcounter{月数}{2}
\setcounter{page}{1}

\発表{2016}{8}{10}

\def\ipsjsigpronumb{76}
%\def\onlineipsjsigpronumb{36}		% ipsjsigpronumb-36 ???

\begin{document}

\title{Continuation based C を用いたプログラムの検証手法}

\etitle{Verification method of programs using Continuation based C}

\affiliate{RUnivIe}{琉球大学 大学院 理工学研究科 情報工学専攻\\
Infomation Engineering Course, Graduate School of Engineering and Science, University of the Ryukyus, 1 Senbaru, Nishihara-cho, Nakagami-gun, Okinawa 903-0213, Japan}

\affiliate{RUniv}{琉球大学\\
University of the Ryukyus}

\author{比嘉 健太}{Yasutaka Higa}{RUnivIe}[atton@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji Kono}{RUniv}[kono@ie.u-ryukyu.ac.jp]

% 和文/英文概要は、発表当日資料に基づく

\begin{abstract}
ソフトウェアが期待される仕様を満たしているか調べることは重要である。特
に実際に動作しているソフトウェア自体を検証できると良い。従来はassert
などを用いて検証しているが、モデル検査のような網羅的な検査を行うことは
できない。そこでソフトウェアの実行自体を網羅的に行うように変更する。こ
れは計算自体を変更するのでメタ計算となる。本研究ではプログラムを
Continuation based C (CbC)で記述する。CbC ではCode Segment という単位
で処理を記述する。CbC を用いることによりメタ計算はCbC のCode Segment
間にMeta Code Segment を挟むという単純な方法で実現できる。そして、通常
計算との切り替えも簡単に行うことができる。ここでは、赤黒木を実際の例題
として検証した。比較対象としてANSI-C の記号実行を行うCBMC でも検証する。
CBMC よりも広い範囲の検査が行えることを確認した。
\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.
\end{eabstract}

\maketitle

\end{document}