changeset 121:606d78b8043e

Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 22 Dec 2015 18:00:05 +0900
parents b210051ca507
children 8bee87dcc403
files .hgignore slides/20151222/slide.md
diffstat 2 files changed, 55 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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
 
--- /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: -->