# HG changeset patch # User Yasutaka Higa # Date 1397551486 -32400 # Node ID c7d57cf16fdb83494742d47a89f8289058502517 # Parent 32cbe5f209f19a4b5838b3add42582e9bcc2157a Update template diff -r 32cbe5f209f1 -r c7d57cf16fdb template/slide.md --- a/template/slide.md Tue Apr 08 17:08:56 2014 +0900 +++ b/template/slide.md Tue Apr 15 17:44:46 2014 +0900 @@ -1,14 +1,15 @@ -title: プログラムから証明の自動生成(仮) +title: プログラムのデバッグ支援(仮) author: Yasutaka Higa cover: lang: Japanese + # 研究目的(仮) -* プログラムの正しさを保証したい -* 既存のプログラムから証明支援系に変換できれば挙動を保証できる? -* 既存のプログラムのターゲットとしてはコードセグメントがある -* 挙動が保証されたプログラムの組み合せでプログラム全体を構成する +* プログラムのデバッグは複雑になることがある +* 例えば、あるif文の条件を満たすには、必要な状態がある +* そういった状態を自動で導出したい +* model checking を使えばいける? # hoge