Mercurial > hg > Members > atton > seminar_slides

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