Mercurial > hg > Members > atton > seminar_slides
comparison slides/20160607/slide.md @ 145:f8a9617b4a37
Add slide for seminar
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Jun 2016 18:14:09 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 144:47c50e759033 | 145:f8a9617b4a37 |
|---|---|
| 1 title: Verification of programs using Continuation based C | |
| 2 author: Yasutaka Higa | |
| 3 profile: | |
| 4 lang: Japanese | |
| 5 | |
| 6 | |
| 7 # 研究目的 | |
| 8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する | |
| 9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される | |
| 10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する | |
| 11 | |
| 12 # 研究内容 | |
| 13 * コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう | |
| 14 * コードセグメントどうしの接続の間にメタ計算として検証機構を導入する | |
| 15 * コードを検証用に変更することなく、仕様を満たすか検証する | |
| 16 * 検証の対象として Gears OS のデータ構造を用いる | |
| 17 | |
| 18 # 近況報告 | |
| 19 * cbmc で llrb を検証する | |
| 20 * nondet_int() があったのでいけそうです | |
| 21 | |
| 22 # cbmc で llrb の検証 | |
| 23 * cbmc は c のコードの symbolic execution なので C syntax にしないといけない | |
| 24 * なのでcbc -> c に変換 | |
| 25 * 具体的には code と goto の置換 | |
| 26 * clang でコンパイル可能な状態まで書けました(syntax valid + executable) | |
| 27 * あとは assert を書いて cbmc でチェックしてやる | |
| 28 | |
| 29 # あとやること | |
| 30 * cbmc のコードに assert を埋め込んで検証 | |
| 31 * 仮に書いている C function を全部 cs に変換する | |
| 32 * JavaPathFinder + AVL-Tree in Java | |
| 33 * synchronized queue の akasha での検証 | |
| 34 * bounded/unbounded | |
| 35 * 論文提出締切: 2016/07/08 | |
| 36 | |
| 37 | |
| 38 <!-- vim: set filetype=markdown.slide: --> |