Mercurial > hg > Members > atton > seminar_slides

comparison template/slide.md @ 163:b8e16c48a5a4 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update template
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 17 Jan 2017 17:18:41 +0900
parents c8ae70995b29
children
comparison
equal deleted inserted replaced
162:725eabd2f778 163:b8e16c48a5a4
1 title: Verification method of programs using Continuation based C 1 title: メタ計算を用いた Continuation based C の検証手法
2 author: Yasutaka Higa 2 author: Yasutaka Higa
3 profile: 3 profile:
4 lang: Japanese 4 lang: Japanese
5 5
6 6
7 # 研究目的 7 # 研究目的
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する 8 * 動作するプログラムの信頼性を保証したい
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される 9 * そのためにコードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する 10 * 処理の単位であるコードセグメントはメタ計算によって相互に接続される
11 * メタ計算を切り替えることでコードセグメントを変更することなくプログラムの性質を検証する
11 12
12 # 研究内容 13 # 研究内容
13 * コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう
14 * コードセグメントどうしの接続の間にメタ計算として検証機構を導入する
15 * コードを検証用に変更することなく、仕様を満たすか検証する 14 * コードを検証用に変更することなく、仕様を満たすか検証する
16 * 検証の対象として Gears OS のデータ構造を用いる 15 * 検証にはコードの状態を数え上げるモデル検査と証明の両方を用いる
16 * モデル検査はコードセグメントの接続部分を変更することで実現する
17 * 証明は Continuation based C 上のコードセグメントを Agda 上で記述した上で証明する
18 * Agda 上でコードセグメントを記述するために CbC の型を部分型として定義する
17 19
18 # hoge 20 # hoge
19 * fuga 21 * fuga
20 22
21 # hogehoge 23 # hogehoge