# HG changeset patch # User Yasutaka Higa # Date 1395740284 -32400 # Node ID 8efe9eb8758b45eafabc6d1b700510770d99e277 # Parent fb9d19430363eaa9909b59b40118ee679bec4cde Update template diff -r fb9d19430363 -r 8efe9eb8758b slides/20140325/slide.md --- a/slides/20140325/slide.md Tue Mar 25 17:55:39 2014 +0900 +++ b/slides/20140325/slide.md Tue Mar 25 18:38:04 2014 +0900 @@ -1,4 +1,4 @@ -title: 証明によるプログラムの信頼性の向上(仮) +title: プログラムから証明の自動生成(仮) author: Yasutaka Higa cover: lang: Japanese diff -r fb9d19430363 -r 8efe9eb8758b template/slide.md --- a/template/slide.md Tue Mar 25 17:55:39 2014 +0900 +++ b/template/slide.md Tue Mar 25 18:38:04 2014 +0900 @@ -1,14 +1,14 @@ -title: 証明によるプログラムの信頼性の向上(仮) +title: プログラムから証明の自動生成(仮) author: Yasutaka Higa cover: lang: Japanese - # 研究目的(仮) -* 証明によるプログラムの信頼性の向上を目指す。 -* 信頼性とは、プログラムがプログラマの予期しない動作をしないことである。 -* 目標の例としては、現在は実行時にしか検出できないエラーなどを実行以前に検出することがある。 +* プログラムの正しさを保証したい +* 既存のプログラムから証明支援系に変換できれば挙動を保証できる? +* 既存のプログラムのターゲットとしてはコードセグメントがある +* 挙動が保証されたプログラムの組み合せでプログラム全体を構成する # hoge