# Date 1462265072 -32400 # Node ID e88c772d72f30e424362f0e68639bf5218db800e # Parent 7b69ffd8598992f72afdbbda1974769cadacdf7e auto-Update generated slides by script diff -r 7b69ffd85989 -r e88c772d72f3 slides/20160503/slide.html --- a/slides/20160503/slide.html Tue May 03 17:42:51 2016 +0900 +++ b/slides/20160503/slide.html Tue May 03 17:44:32 2016 +0900 @@ -2,10 +2,10 @@ - <%= @headers['title'] %> + Verification of programs using Continuation based C - - + + @@ -38,7 +38,7 @@ prettyPrint(); } ); - <%= content_for :js %> + @@ -46,7 +46,7 @@ -<%= content_for :head %> + @@ -67,15 +67,15 @@

<%= @headers['title'] %>

Verification of programs using Continuation based C

- <%= @headers['author'] %> - <%= @headers['profile'] %> + Yasutaka Higa +

@@ -83,7 +83,106 @@ -<%= @content %> +

+ + + +

研究目的

コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
プログラムはコードセグメントという処理の集合として表され、相互に接続される
個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する

+ + +

+ +

研究内容

コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう
コードセグメントどうしの接続の間にメタ計算として検証機構を導入する
コードを検証用に変更することなく、仕様を満たすか検証する
検証の対象として Gears OS のデータ構造を用いる

+ + +

+ +

近況報告

SWoPP のネタ +
- Gears のデータ構造の検証
- Operational Semantics of CbC
+
発表申込締切が 2016/05/13 あたりなので来週くらいに発表アブストを持ってきます

+ + +

+ +

Gears のデータ構造の検証

Red-Black Tree +
- insertion の全探索は13要素までOK
- 6,227,020,800 通り
+
Synchronized Queue +
- bounded queue +
  - 各 thread が取りえる操作を全探索
  +
- unbounded queue +
  - アイデア: 0, 1, 2 以上で抽象化
  +
+

+ + +

+ +

Operational Semantics of CbC

Agda で CbC を書けるか
memory allocation 部分とかは meta に押しつけて書く +
- 待ちあわせとかも無い
+
cs は ds -> ds +
- +
  それだと行き先情報が無いので
  +
- +
  ds に next を含める or State Monad 辺りでやってみる
  +
+
Agda を 2.5.1 に上げて State Monad を書いてみてます

+ + + +

+ diff -r 7b69ffd85989 -r e88c772d72f3 slides/20160503/slide.md --- a/slides/20160503/slide.md Tue May 03 17:42:51 2016 +0900 +++ b/slides/20160503/slide.md Tue May 03 17:44:32 2016 +0900 @@ -39,6 +39,6 @@ * それだと行き先情報が無いので * ds に next を含める or State Monad 辺りでやってみる -* Agda を 2.5.1 に上げて State Monad を書いてみてるところ +* Agda を 2.5.1 に上げて State Monad を書いてみてます