--- a/template/slide.md	Mon Apr 27 18:33:10 2015 +0900
+++ b/template/slide.md	Tue Apr 28 16:59:46 2015 +0900
@@ -1,20 +1,19 @@
-title: Categorical Formalization of Program Modification
+title: Verification of programs using Code Segments and Data Segments
 author: Yasutaka Higa
 profile:
 lang: Japanese
 
 
-# 研究目的 (Categorical Formalization)
-* プログラムの信頼性を向上させるために開発手法に着目する
-* プログラムの信頼性が変化するのはプログラムを変更した時である
-* 信頼性を保ちながらプログラムを変更にプログラムの変更を形式化する
-* Kleisli Category の Kleisli Triple と対応のある Monad によってプログラムの変更を記述する
+# 研究目的
+* コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
+* プログラムはコードセグメントという処理の集合として表され、相互に接続される
+* 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
 
-# 研究目的 (Parallel Debugger)
-* 本研究では Monad を用いてプログラムの変更を定義する
-* Monad とは meta computation とデータ構造を対応付ける手法である
-* プログラムの変更は変更前の動作を保存しつつ変更後の動作を追加することで表現する
-* 異なるバージョンのプログラムを同時に実行し、トレースを比較することでデバッグを支援する手法を提案する
+# 研究内容
+* コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
+* 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
+* 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
+* メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する
 
 # hoge
 * hoge