title: メタ計算を用いた Continuation based C の検証手法
author: Yasutaka Higa
profile:
lang: Japanese


# 研究目的
* 動作するプログラムの信頼性を保証したい
* そのためにコードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
* 処理の単位であるコードセグメントはメタ計算によって相互に接続される
* メタ計算を切り替えることでコードセグメントを変更することなくプログラムの性質を検証する

# 研究内容
* コードを検証用に変更することなく、仕様を満たすか検証する
* 検証にはコードの状態を数え上げるモデル検査と証明の両方を用いる
* モデル検査はコードセグメントの接続部分を変更することで実現する
* 証明は Continuation based C 上のコードセグメントを Agda 上で記述した上で証明する
* Agda 上でコードセグメントを記述するために CbC の型を部分型として定義する

# hoge
* fuga

# hogehoge
* fugafuga


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