# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1450774805 -32400
# Node ID 606d78b8043e94642fab93cdc0fc39869bcb1b2f
# Parent  b210051ca507bf7002271e026231f0b4fdf42e82
Add slide for seminar

diff -r b210051ca507 -r 606d78b8043e .hgignore
--- a/.hgignore	Tue Dec 22 17:59:35 2015 +0900
+++ b/.hgignore	Tue Dec 22 18:00:05 2015 +0900
@@ -9,6 +9,8 @@
 *.css
 *.html
 
+images/*.svg
+
 pictures/*.svg
 pictures/*.jpg
 
diff -r b210051ca507 -r 606d78b8043e slides/20151222/slide.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20151222/slide.md	Tue Dec 22 18:00:05 2015 +0900
@@ -0,0 +1,53 @@
+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: -->