annotate template/slide.md @ 116:ac66893b6be1

Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 24 Nov 2015 18:14:27 +0900
parents b9664a92428d
children 2e11c520fa17
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
103
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
1 title: Verification of programs using Code Segments and Data Segments
9
8cd28e3368fd Use shower template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
2 author: Yasutaka Higa
87
27f7f51b135e Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
3 profile:
9
8cd28e3368fd Use shower template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
4 lang: Japanese
8cd28e3368fd Use shower template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
5
37
c7d57cf16fdb Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
6
103
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
7 # 研究目的
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
87
27f7f51b135e Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 76
diff changeset
11
103
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
12 # 研究内容
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
13 * コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
14 * 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
15 * 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
b9664a92428d Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
16 * メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する
28
4d583de693b3 Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
17
7
e0c4a349c94f Copy template when generate new slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 # hoge
28
4d583de693b3 Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
19 * hoge
4d583de693b3 Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
20 * hogehoge
9
8cd28e3368fd Use shower template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
21
8cd28e3368fd Use shower template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
22 # fuga
28
4d583de693b3 Update template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
23 * fuga
9
8cd28e3368fd Use shower template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
24 * fugafuga
32
cc91543302b3 Set filetype on slide template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
25
cc91543302b3 Set filetype on slide template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
26 <!-- vim: set filetype=markdown.slide: -->