title: Verification of programs using Code Segments and Data Segments
author: Yasutaka Higa
profile:
lang: Japanese


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

# 研究内容
* コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
* 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
* 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
* メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する

# 近況報告
* ie-virsh について
* slideshow-s6cr
* CbC/DPP

# ie-virsh について
* ブログ見て状況把握しました?
* 想定してる課題?
* kernel debug できる xml を定義できる形でOKですかね
* ポートが決めうち or ユーザ指定
* uid くらいでOK?

# slideshow-s6cr
* ssh://firefly.cr.ie.u-ryukyu.ac.jp/~one/hg/Members/atton/slideshow-s6cr
* 徳森さんのスライドをベースにしてます
* Chrome の file:// 問題も解決済み
* 拡大縮小可能 + アウトラインモード付き
* prettify.js で sytax highlight もサポートしてます

```
int main(void) {
    puts("hello");
}
```

# CbC/DPP
* Dining Philosophers Problem
* CVS から hg に移しました (ssh://firefly.cr.ie.u-ryukyu.ac.jp/hg/CbC/DPP)
* dpp, dpp2, tableau, tableau2, tableau3 があります
* dpp, dpp2 までは compile 通しました
    * dpp は philosopher1 のみが行動
    * dpp2 は全 philosopher が動いて最速でデッドロック
* tableau は compile error が出ます


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