# HG changeset patch # User Yasutaka Higa # Date 1458637813 -32400 # Node ID 2e11c520fa17045c44d8ed7347d6ce62df09d372 # Parent 671367495f984cc4ca060947d1aa4a428f491f81 Update template diff -r 671367495f98 -r 2e11c520fa17 template/slide.md --- a/template/slide.md Tue Mar 15 18:23:38 2016 +0900 +++ b/template/slide.md Tue Mar 22 18:10:13 2016 +0900 @@ -1,4 +1,4 @@ -title: Verification of programs using Code Segments and Data Segments +title: Verification of programs using Continuation based C author: Yasutaka Higa profile: lang: Japanese @@ -10,17 +10,16 @@ * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する # 研究内容 -* コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する -* 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる -* 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する -* メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する +* コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう +* コードセグメントどうしの接続の間にメタ計算として検証機構を導入する +* コードを検証用に変更することなく、仕様を満たすか検証する +* 検証の対象として Gears OS のデータ構造を用いる # hoge -* hoge -* hogehoge +* fuga -# fuga -* fuga +# hogehoge * fugafuga +