Mercurial > hg > Members > atton > seminar_slides

annotate slides/20160510/slide.md @ 142:bc0c33dbfe69

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 10 May 2016 18:15:10 +0900
parents
children d50b8510fbdd
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
142
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Verification of programs using Continuation based C
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 profile:
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 # 研究目的
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 # 研究内容
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 * コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 * コードセグメントどうしの接続の間にメタ計算として検証機構を導入する
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * コードを検証用に変更することなく、仕様を満たすか検証する
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * 検証の対象として Gears OS のデータ構造を用いる
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 # 近況報告
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 * SWoPP2016 申し込み [2016/05/09-13](https://sigpro.ipsj.or.jp/#schedule110)
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * 申し込みアブスト書いたのでチェックお願いします
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 * 論文に向けて今後やることリスト
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 # 論文タイトル
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 * 和文: Verification of programs using Continuation based C
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 * verificatoin method of ~ でも良いかなとか
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 * 英文: Continuation based C を用いたプログラムの検証
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 # 和文アブスト(600文字程度)
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 * Continuation based C 言語によって記述されたプログラムのデータ構造の性質を検証する手法を提案する。
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 * Continuation based C とは当研究室が提案している Code Segment, Data Segment という単位でプログラムを記述する言語である。
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 * Code Segment とは処理の単位であり、データの単位である Data Segment を入力と出力に持つ。
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 * プログラム全体は Code Segment どうしの接続により表現され、あるCode Segment の出力は接続された次の Code Segment の入力となる。
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 * また、メモリ管理やエラーの処理など、本来中心に行ないたい処理と異なる処理はメタ計算として分離し、Meta Code Segment, Meta Data Segment として記述する。
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 * Code Segment の接続処理を Meta Code Segment として表現し、接続部分に検証を含めることで 元の Code Segment を変更することなくプログラムの検証を行なう。
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 * 本論文では Continuatoin based C によって記述された赤黒木や Synchronized Queue といったデータ構造の性質を検証する。
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 # 英文アブスト(200 words) (ちょっと足りてない)
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 * We propose a verification method for programs using Continuation based C language.
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 * Our laboratory develops Continuation based C language which supports programming unit called Code Segment, Data Segment.
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 * Code segments that the calculation unit has input/output data segment that data unit.
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 * Programs are represented by connections between code segment and code segment.
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 * The output data segment of some code segment is converts to the input data segment of connected one.
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 * Programming paradigm using Code segments splits main computations and complicated computations such as memory control, error handling and more to meta computations.
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 * Meta computations represented to meta code segment and meta data segment, which saves main computations.
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 * 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.
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 # 論文作成に向けて今後やることリスト
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 * 論文提出締切: 2016/07/08
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 * 仮に書いている function を全部 cs に
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 * synchronized queue の検証
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 * bounded/unbounded
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
bc0c33dbfe69 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 <!-- vim: set filetype=markdown.slide: -->