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


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

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

# 近況報告
* シス管次期WebConsole作成中
* bind の連携まで終了
    * v4/v6 正引き/逆引き まで
    * IPv6 もフィルタリングされます
* 今VM貸出フォームで kvm のイメージをクローンする機能を実装中
    * fog + fog-libvirt を触ってます

# 詰まってるところ
* 何故が Rails の pg が Linux で動かない
* PG::ConnectionBad: PQsocket() can't get socket descriptor
    * PostgreSQL のサーバはMac/Linux共に同じコンテナを使用
    * PostgreSQL の server/client を 9.1/9.2/9.3/9.4 にしてもダメ
        * Mac だとバージョンを変えてもOK
    * 実機/Docker/VirtualBox でもダメ(仮想環境の問題では無い?)
    * CentOS/Fedora でもダメ(kernel では無い?)


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