# HG changeset patch # User Yasutaka Higa # Date 1481442959 -32400 # Node ID c73e1ee2d5ee57244d47d48ec1c8167710da0340 # Parent f5cad08f76b58f1db00b5e51557cee413db49920 Import abstract for proceedings diff -r f5cad08f76b5 -r c73e1ee2d5ee abstract/03higa_ryukyu.txt --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/abstract/03higa_ryukyu.txt Sun Dec 11 16:55:59 2016 +0900 @@ -0,0 +1,84 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%% プログラミング研究会・発表申込みフォーム %%%%%%%% +%%%%%%%% %%%%%%%% +%%%%%%%% 以下の記入例を削除して記入してください %%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%% 氏名・所属（和文および英文，発表者に○印をつけて下さい） +\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 diff -r f5cad08f76b5 -r c73e1ee2d5ee abstract/abst5_higa.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/abstract/abst5_higa.tex Sun Dec 11 16:55:59 2016 +0900 @@ -0,0 +1,61 @@ +\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}