Mercurial > hg > Members > atton > seminar_slides
annotate template/slide.md @ 163:b8e16c48a5a4 default tip
Update template
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 17 Jan 2017 17:18:41 +0900 |
parents | c8ae70995b29 |
children |
rev | line source |
---|---|
163 | 1 title: メタ計算を用いた Continuation based C の検証手法 |
9
8cd28e3368fd
Use shower template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
2 author: Yasutaka Higa |
87 | 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 | 6 |
103 | 7 # 研究目的 |
163 | 8 * 動作するプログラムの信頼性を保証したい |
9 * そのためにコードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する | |
10 * 処理の単位であるコードセグメントはメタ計算によって相互に接続される | |
11 * メタ計算を切り替えることでコードセグメントを変更することなくプログラムの性質を検証する | |
87 | 12 |
103 | 13 # 研究内容 |
131 | 14 * コードを検証用に変更することなく、仕様を満たすか検証する |
163 | 15 * 検証にはコードの状態を数え上げるモデル検査と証明の両方を用いる |
16 * モデル検査はコードセグメントの接続部分を変更することで実現する | |
17 * 証明は Continuation based C 上のコードセグメントを Agda 上で記述した上で証明する | |
18 * Agda 上でコードセグメントを記述するために CbC の型を部分型として定義する | |
28 | 19 |
7
e0c4a349c94f
Copy template when generate new slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 # hoge |
131 | 21 * fuga |
9
8cd28e3368fd
Use shower template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
22 |
131 | 23 # hogehoge |
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 |
131 | 26 |
32
cc91543302b3
Set filetype on slide template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
27 <!-- vim: set filetype=markdown.slide: --> |