\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 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

\end{document}