title: Verification of programs using Code Segments and Data Segments
author: Yasutaka Higa
profile:
lang: Japanese


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

# 研究内容
* コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
* 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
* 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
* メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する

# 近況報告
* ie-virsh に define-gdb コマンドを追加
* Gears の llrb に木の高さを assert するだけの meta cs を記述

# ie-virsh に define-gdb コマンドを追加
* ie-virsh define-gdb 01
* とすると
    * -S -gdb tcp::12345
    * のようなオプションが有効になった xml を生成します
* port は 10000,30000 の間でランダム
* gdb で attach できるのまでは確認しましたが、 linux-kernel 4.4-rc5 はそもそも起動しない
    * fedora23 に rsync して make modules_install install したが起動せず
    * grub2.cfg には書き込まれてる
    * boot の途中で止まる

# llrb with put assert
* 次の action が put なら高さをチェックしてから次の cs という meta を定義
    * llrb のコードは全く変更せず
* 2 * min height < max height
* になっているかをチェックするだけ
* insert 回数 2万は耐えてました
* 状態の抽象化をどうするか……

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