Mercurial > hg > Members > atton > seminar_slides

annotate slides/20150421/slide.md @ 100:aede1f893abb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 21 Apr 2015 18:00:32 +0900
parents
children 12d14098c035
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
100
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Verification of programs using Code Segments Data Segments
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 profile:
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 # 研究目的
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうし組み合わせによりプログラム全体を検証する
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 # 研究内容
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 * コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 * 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * 計算とメタ計算の対応には Monad を用い、計算が存在すればメタ計算が存在することを保証する
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 # Summary
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 * LOLA 2015 提出しました
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * おそらく間にあってます
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 * 研究計画書に書く項目があるのでコメントとかください
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 * 研究題目, 研究目的, 研究内容, 研究計画
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 * 指導教官コメント, 副指導教官コメント
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 # 研究計画書(研究題目と研究目的)
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 * 研究題目
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 * Verification of programs using Code Segments Data Segments
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 * 研究目的
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 * 当研究室で提唱しているコードセグメントとデータセグメントを用いたプログラムに対し、形式的な検証を行なうことでプログラムの信頼性を保証する。
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 # 研究計画書の項目(研究内容と研究計画)
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 * 研究内容
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 * コードセグメントとデータセグメントを用いて記述したプログラムに対し、メタ計算として検証を行なう。
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 * メタ計算の形式化にはMonadを用い、モデルチェッカーや証明、プログラムの変更などを言語機構に組込む。
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 * 研究計画
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 * プログラムの変更の形式化 - 6月まで
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 * LOLA 2015 にて発表する (6月)
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 * モデルチェッカーのサーベイと実装 - 前期終了時目処
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
aede1f893abb Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 <!-- vim: set filetype=markdown.slide: -->