Mercurial > hg > Members > atton > seminar_slides

comparison template/slide.md @ 131:2e11c520fa17

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update template
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 22 Mar 2016 18:10:13 +0900
parents b9664a92428d
children c8ae70995b29
comparison
equal deleted inserted replaced
130:671367495f98 131:2e11c520fa17
1 title: Verification of programs using Code Segments and Data Segments 1 title: Verification of programs using Continuation based C
2 author: Yasutaka Higa 2 author: Yasutaka Higa
3 profile: 3 profile:
4 lang: Japanese 4 lang: Japanese
5 5
6 6
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する 8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される 9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する 10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
11 11
12 # 研究内容 12 # 研究内容
13 * コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する 13 * コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう
14 * 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる 14 * コードセグメントどうしの接続の間にメタ計算として検証機構を導入する
15 * 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する 15 * コードを検証用に変更することなく、仕様を満たすか検証する
16 * メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する 16 * 検証の対象として Gears OS のデータ構造を用いる
17 17
18 # hoge 18 # hoge
19 * hoge 19 * fuga
20 * hogehoge
21 20
22 # fuga 21 # hogehoge
23 * fuga
24 * fugafuga 22 * fugafuga
25 23
24
26 <!-- vim: set filetype=markdown.slide: --> 25 <!-- vim: set filetype=markdown.slide: -->