Mercurial > hg > Members > atton > seminar_slides

comparison slides/20170117/slide.md @ 162:725eabd2f778

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide for seminar
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 17 Jan 2017 17:18:01 +0900
parents
children
comparison
equal deleted inserted replaced
161:fa9c8783024b 162:725eabd2f778
1 title: メタ計算を用いた Continuation based C の検証手法
2 author: Yasutaka Higa
3 profile:
4 lang: Japanese
5
6
7 # 研究目的
8 * 動作するプログラムの信頼性を保証したい
9 * そのためにコードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
10 * 処理の単位であるコードセグメントはメタ計算によって相互に接続される
11 * メタ計算を切り替えることでコードセグメントを変更することなくプログラムの性質を検証する
12
13 # 研究内容
14 * コードを検証用に変更することなく、仕様を満たすか検証する
15 * 検証にはコードの状態を数え上げるモデル検査と証明の両方を用いる
16 * モデル検査はコードセグメントの接続部分を変更することで実現する
17 * 証明は Continuation based C 上のコードセグメントを Agda 上で記述した上で証明する
18 * Agda 上でコードセグメントを記述するために CbC の型を部分型として定義する
19
20 # 近況報告
21 * 部分型を使って定義した CS/DS のコードで n回 push して n回 pop すると戻る証明が書けました
22 * AMS-Tex は amsmath を使えば良さそうです
23 * 修論の目次を書きました
24 * グローバル公開しているサーバが攻撃を受けたようです
25 * pukiwiki への攻撃。再監査などの動きもあると思います。
26
27 # n-push/n-pop
28 * 『任意のスタックに対して同じ回数だけ push して pop すると元に戻る』
29 * 定義できましたが、前提がいくつかあります
30 * たぶんこの前提を得られることの方に意味があると思っています
31 * push する要素を指定せずに push/pop すると一回popされてしまう
32 * 今のコードは要素を指定しないと push しない
33 * 実装依存のコードを証明できたので割と良い結果だと思っています
34 * continuation の処理内容によっては context は変更される
35 * ので refl にならない『時もある』
36
37 # 修論の目次
38 * [Mercurial/hg/Papers/2017/atton-master ](http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2017/atton-master/)
39 * チェックお願いします
40
41 # AMS-TeX
42 * [amstex](https://www.ctan.org/pkg/amstex)
43 * American Mathematical Society plain TeX macros
44 * 今は [AMS-LaTeX](https://www.ctan.org/pkg/amslatex) があるようです
45 * 具体的には amsmath package
46 * MacTeX 20161009 でも利用可能
47
48 <!-- vim: set filetype=markdown.slide: -->