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


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

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

# 近況報告
* IPSJ-PRO 申し込みました
* CBMC の環境を作りました

# CBMC
* akasha の対抗馬の一つとして
* [CBMC](http://www.cprover.org/cbmc/) is bounded Model checker for C and C++ programs.
* 環境を構築した Dockerfile を repository に入れてあります

# CBMC tutorial
* [short tutorial](http://www.cprover.org/cprover-manual/cbmc.shtml)
* SEGV の検出とか loop unwinding とか
* assert が落ちる条件も出してくれたので assert で書く形にしようかなと
* C を symbolic simulation するので syntax valid な C program でないといけない

# CBMC + cbc
* cbc のコードを cbmc で実行してみる
* goto を return に、 code を void に
    * これで基本的には大丈夫。あとは場合によりけり。
* llrb もそのまま動かせました
* C の synbolic simulation なので link とかせずに必要なファイルを全て指定する
    * $ cbmc -I../include -Iinclude llrb.c  main.c origin_cs.c stack.c allocate.c compare.c llrbContext.c --unwind 5  --bounds-check --pointer-check --unwinding-assertions
* 10 分くらい動かしてますけど終わらない

# あとやること
* JavaPathFinder + AVL-Tree in Java
* 仮に書いている function を全部 cs に変換する
* synchronized queue の akasha での検証
    * bounded/unbounded
* 論文提出締切: 2016/07/08


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