title: Verification of programs using Continuation based C
author: Yasutaka Higa
profile:
lang: Japanese


# 研究目的
* コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
* プログラムはコードセグメントという処理の集合として表され、相互に接続される
* 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する

# 研究内容
* コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう
* コードセグメントどうしの接続の間にメタ計算として検証機構を導入する
* コードを検証用に変更することなく、仕様を満たすか検証する
* 検証の対象として Gears OS のデータ構造を用いる

# 近況報告
* SWoPP2016 申し込み [2016/05/09-13](https://sigpro.ipsj.or.jp/#schedule110)
* 申し込みアブスト書いたのでチェックお願いします
* 論文に向けて今後やることリスト

# 論文タイトル
* 和文: Verification of programs using Continuation based C
    * verificatoin method of ~ でも良いかなとか
* 英文: Continuation based C を用いたプログラムの検証

# 和文アブスト(600文字程度)
* 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 といったデータ構造の性質を検証する。

# 英文アブスト(200 words) (ちょっと足りてない)
* 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 that the calculation unit has input/output data segment that data unit.
* Programs are represented by connections between code segment and code segment.
* The output data segment of some code segment is converts to the input data segment of connected one.
* Programming paradigm using Code segments splits main computations and complicated computations such as memory control, error handling and more to meta computations.
* Meta computations represented to meta code segment and meta data segment, which saves main computations.
* In this paper, 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.

# 論文作成に向けて今後やることリスト
* 論文提出締切: 2016/07/08
* 仮に書いている function を全部 cs に
* synchronized queue の検証
    * bounded/unbounded

<!-- vim: set filetype=markdown.slide: -->