%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%% プログラミング研究会・発表申込みフォーム %%%%%%%%

%%%%%%%%                                          %%%%%%%%

%%%%%%%% 以下の記入例を削除して記入してください   %%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%%% 氏名・所属（和文および英文，発表者に○印をつけて下さい）

\author{○比嘉 健太}{Yasutaka HIGA}{RUnivIe}[atton@cr.ie.u-ryukyu.ac.jp]

\author{河野 真治}{Shinji KONO}{RUniv}[kono@ie.u-ryukyu.ac.jp]



% 注:   和文，欧文の氏名の後に所属ラベルをつけて，以下で定義してください．

%       氏と名の間はスペースを一つ空けてください．

%       所属が複数の場合はラベルをカンマで区切り，並べてください．

%       全角スペースは用いないでください．





% 所属ラベルの定義 (和文と英文は「\\ 」で区切ってください)

\affiliate{RUnivIe}{琉球大学 大学院 理工学研究科 情報工学専攻\\

Infomation Engineering Course Graduate School of Engineering and Science University of the Ryukyus}



\affiliate{RUniv}{琉球大学\\

University of the Ryukyus}





%%% 代表者連絡先（氏名，住所，電話，Fax，電子メールアドレス）

\contact{

比嘉 健太

琉球大学 工学部 情報工学科

〒903-0213 沖縄県西原町千原１番地 琉球大学情報工学科

Tel: 098-895-8662, Fax: 098-895-8727

E-mail: atton@cr.ie.u-ryukyu.ac.jp

}





%%% タイトル（和文論文の場合は和文と英文の両方）

% 和文タイトル

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



% 英文タイトル

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





%%% 発表概要（和文600字程度，英文200ワード程度．和文論文の場合は和文と

%%%          英文の両方を添付するものとし，英文論文の場合は英文が必須です．）



% 和文発表概要 (600字程度)
\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 によって記述された赤黒木や Synchronized Queue といったデータ構造の性質を検証する。
\end{abstract}

% 英文発表概要 (200ワード程度)
\begin{eabstract}
We propose a verification method for 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 presentation, We define a meta computation which connects code segments with verifications and verify properties of data structures such as Red-Black Tree and Synchironized Queue.
\end{eabstract}

%%% 論文誌投稿を希望の有無 （どちらか残してください）

% 希望する



%%% オリジナル論文とサーベイ論文の種別指定  （どちらか残してください）

% オリジナル論文



%%% 発表者の年度冒頭(4月1日)の年齢  （どちらか残してください）

% 29歳以下



%%%%%% ここまでプログラミング研究会・発表申し込みフォーム %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



-----------

琉球大学 理工学研究科 情報工学専攻 2年次 並列信頼研所属

比嘉健太 (Yasutaka HIGA)

atton@cr.ie.u-ryukyu.ac.jp <mailto:atton@cr.ie.u-ryukyu.ac.jp>