Mercurial > hg > Members > atton > seminar_slides
changeset 131:2e11c520fa17
Update template
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 22 Mar 2016 18:10:13 +0900 |
parents | 671367495f98 |
children | aff7d9073d5d |
files | template/slide.md |
diffstat | 1 files changed, 8 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/template/slide.md Tue Mar 15 18:23:38 2016 +0900 +++ b/template/slide.md Tue Mar 22 18:10:13 2016 +0900 @@ -1,4 +1,4 @@ -title: Verification of programs using Code Segments and Data Segments +title: Verification of programs using Continuation based C author: Yasutaka Higa profile: lang: Japanese @@ -10,17 +10,16 @@ * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する # 研究内容 -* コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する -* 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる -* 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する -* メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する +* コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう +* コードセグメントどうしの接続の間にメタ計算として検証機構を導入する +* コードを検証用に変更することなく、仕様を満たすか検証する +* 検証の対象として Gears OS のデータ構造を用いる # hoge -* hoge -* hogehoge +* fuga -# fuga -* fuga +# hogehoge * fugafuga + <!-- vim: set filetype=markdown.slide: -->