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


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

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

# 近況報告
* kernel build しました。 gdb での trace まで確認しました。
* llcov は動かなかったです
* Gears の Dockerfile 作りました
* さくらの課題が出ました

# Kernel build
* linux kernel 4.4-rc5 を debug option 付きでビルド
* /net/home/open/LinuxKernel/linux-4.4-rc5 にあります
* make menuconfig
* make -j 8
* make modules_install install とか
* ie-virsh define-gdb した VM で trace できることを確認しました

# llcov
* 公式パッケージでは無いっぽいです
* [https://github.com/choller/LLCov](https://github.com/choller/LLCov) にあります
* 3.4, 3.5, 3.6 supported で CbC_llvm は 3.8 based
* 案の定 build できず。 Segmentation Fault。

# Gears の Dockerfile
* llcov を試す際にどうせなのでコンテナでやってみました
    * Gears のリポジトリに Dockerfile を追加してあります
* CbC_llvm と llrb は container でも動いてました

# さくらクラウドのVM
* OS の課題が出ました
* やること
    * IPv6 reachable にする
    * 貸し出し用テンプレートを作る
* ちょっとしばらくは動きたくないので他の人に投げたいところ
    * 一応シス管 Redmine には報告済み
    * そろそろ就活で東京へ飛んだりします

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