title: Verification of programs using Continuation based C
author: Yasutaka Higa
profile:
lang: Japanese


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

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

# 近況報告
* llrb の insertion の検証
* 仮に C function で書いていた部分を cs に変換中
    * やってることは木を深さ情報付きで辿る + 辿る+コピー
* 辿る部分は書けたが TCE が失敗してる模様
    * SEGV で落ちるし lldb で bt が取れる
    * Tail call elimination was failed on goto warning: not unreachable instruction in a tail call.
* allocate() してるのがまずそう
* allocate を akasha 内部では cs でやろうかなと考え中

# あとやること
* (doing) 仮に書いている C function を全部 cs に変換する
* cbmc のコードに assert を埋め込んで検証
* JavaPathFinder + AVL-Tree in Java
* synchronized queue の akasha での検証
    * bounded/unbounded
* 論文提出締切: 2016/07/08


<!-- vim: set filetype=markdown.slide: -->