title: プログラムから証明の自動生成(仮)
author: Yasutaka Higa
cover:
lang: Japanese

# 研究目的(仮)

* プログラムの正しさを保証したい
* 既存のプログラムから証明支援系に変換できれば挙動を保証できる？
* 既存のプログラムのターゲットとしてはコードセグメントがある
* 挙動が保証されたプログラムの組み合せでプログラム全体を構成する

# hoge

* hoge
* hogehoge

# fuga

* fuga
* fugafuga

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