Papers/2017/atton-master: presentation/slide.html comparison

comparison presentation/slide.html @ 120:8a84cda440f3

Update slide

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Tue, 14 Feb 2017 11:31:08 +0900
parents	26563097333c
children	137aae675a94

comparison

equal deleted inserted replaced

-:26563097333c
+:8a84cda440f3
 <div class='slide '>
 <!-- === begin markdown block ===
 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-on 2017-02-13 17:40:39 +0900 with Markdown engine kramdown (1.13.0)
+on 2017-02-14 11:30:47 +0900 with Markdown engine kramdown (1.13.0)
 using options {}
 -->
 <!-- _S9SLIDE_ -->
 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">モデル検査的アプローチについての流れ</h1>
+<h1 id="section-2">本発表ではモデル検査的アプローチについて中心に見ていきます</h1>
+<ul>
+<li>修士論文の内部の比率は半分半分くらい</li>
+<li>定理証明の方は説明する内容が多くて複雑</li>
+<li>モデル検査的アプローチは過去論文を提出したもの
+<ul>
+<li>なのでそちらをメインで発表します</li>
+</ul>
+</li>
+</ul>
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-3">モデル検査的アプローチについての流れ</h1>
 <ul>
 <li>Continuation based C (CbC) 言語について</li>
 <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li>
 <li>CbC とメタ計算について</li>
 <li>CbC で記述された GearsOS とそのデータ構造である赤黒木</li>
 <!-- _S9SLIDE_ -->
 <h1 id="codesegment">CodeSegment</h1>
 <ul>
 <li>CodeSegment とは
 <ul>
-<li>処理の単位</li>
+<li>処理の単位であり、入力と出力を持つ</li>
 <li>結合や分割が容易</li>
-<li>入力と出力を持つ</li>
+</ul>
-</ul>
+</li>
-</li>
+<li>CodeSegment どうしを接続することによりプログラム全体を作る
-<li>CodeSegment どうしを接続することによりプログラム全体を作る</li>
+<ul>
+<li>関数呼び出しと違って戻ってこない(goto)</li>
+</ul>
+</li>
 </ul>
 <p><img src="./images/cs.svg" alt="cs" width="50%" /></p>
+<pre><code>__code cs0(int a, int b){
+goto cs1(a+b);
+}
+</code></pre>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
 </li>
 </ul>
 <p><img src="./images/ds.svg" alt="ds" width="50%" /></p>
+<pre><code>__code cs0(int a, int b){
-</div>
+goto cs1(a+b);
-<div class='slide '>
+}
-<!-- _S9SLIDE_ -->
+</code></pre>
-<h1 id="section-3">メタ計算</h1>
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-4">メタ計算</h1>
 <ul>
 <li>とある計算を実現するための計算</li>
 <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
 <li>CbC は通常レベルの計算とメタ計算を分離して考える
 <ul>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-4">赤黒木</h1>
+<h1 id="section-5">赤黒木</h1>
 <ul>
 <li>データの保存に用いる二分木</li>
 <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
 <ul>
 <li>ルートノードと葉ノードの色は黒</li>
 <li>ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定</li>
 </ul>
 </li>
 </ul>
-<p><img src="./images/rbtree.svg" alt="rbtree" width="50%" /></p>
+<p><img src="./images/rbtree.svg" alt="rbtree" width="35%" /></p>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
 <li>GearsOS では木の実装のためにスタックを用いて経路情報を保持している</li>
 </ul>
 <p><img src="./images/put.svg" alt="put" width="50%" /></p>
+<pre><code>goto meta(context, Put);
-</div>
+</code></pre>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="section-5">仕様の記述とその確認</h1>
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-6">仕様の記述とその確認</h1>
 <ul>
 <li>「バランスが取れている」とは何かを表現できる必要がある
 <ul>
 <li>実行可能な CbC の式を使った assert になる</li>
 </ul>
 <li>仕様は bool になる式を用いた assert</li>
 <li>デメリット: promela は C とは記述が異なる</li>
 </ul>
 </li>
 </ul>
+<pre><code>assert(x &lt; 10);
+</code></pre>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
 <li>有限ステップ検証する有界モデル検査器</li>
 </ul>
 </li>
 </ul>
+<pre><code>assert(x &lt; 10);
-</div>
+</code></pre>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="akasha">メタ計算ライブラリ akasha</h1>
+</div>
-<ul>
+<div class='slide '>
-<li>メタ計算としてプログラムの状態を数え上げる
+<!-- _S9SLIDE_ -->
-<ul>
+<h1 id="section-7">チェックする仕様</h1>
-<li>goto された時に挿入される要素の組み合わせを全て列挙して実行する</li>
-<li>その度に仕様の式は成り立つかをチェックする</li>
-</ul>
-</li>
-<li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
-</ul>
-<p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p>
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="section-6">チェックする仕様</h1>
 <ul>
 <li>赤黒木の高さに関する仕様に以下のものがある
 <ul>
 <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
 </ul>
 </li>
-<li>以下のように assert を用いて CbC で定義できる</li>
+<li>以下のような条件式を仕様として CbC で定義、検証できる</li>
-<li>この仕様が満たされるかをチェックする</li>
 </ul>
 <pre><code>__code verifySpecificationFinish(struct Context* context) {
 if (context-&gt;data[AkashaInfo]-&gt;akashaInfo.maxHeight &gt;
 2*context-&gt;data[AkashaInfo]-&gt;akashaInfo.minHeight)
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="akasha">メタ計算ライブラリ akasha</h1>
+<ul>
+<li>メタ計算としてプログラムの状態を数え上げる
+<ul>
+<li>goto された時に挿入される要素の組み合わせを全て列挙して実行する
+<ul>
+<li>赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……</li>
+</ul>
+</li>
+<li>その度に仕様の式は成り立つかをチェックする</li>
+</ul>
+</li>
+<li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
+</ul>
+<p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p>
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="akasha--cbmc-">akasha と CBMC の比較</h1>
 <ul>
 <li>akasha は有限の要素数の組み合わせをチェックする
 <ul>
 <li>要素数が13個までならどの順で木に挿入しても良い</li>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-7">定理証明的なアプローチの流れ</h1>
-<ul>
-<li>プログラムを証明するにはどうするのか</li>
-<li>証明支援系 Agda における証明</li>
-<li>Agda による CbC の定義</li>
-<li>Agda を用いて CbC のコードを証明する</li>
-</ul>
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
 <h1 id="continuation-based-c-">定理証明を Continuation based C へ適用するには</h1>
 <ul>
 <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li>
 <li>そのままプログラムの性質を保証してやる</li>
 <li>Coq, Agda, ATS2 などのプログラミング言語で証明が可能
 </li>
 <li>メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い</li>
 <li>部分型を使う
 <ul>
 <li>Java におけるインターフェース、Haskell における型クラス</li>
-<li>「このデータにはこのフィールドさえあれば良い」</li>
+<li>「このフィールドXがあればデータ型Tとみなして良い」</li>
 </ul>
 </li>
 </ul>
 <ul>
 <li>cs0 の定義はメタ計算用に変更しなくても良い</li>
 </ul>
 </li>
 </ul>
+<pre><code>cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -&gt; goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+</code></pre>
 <pre><code>main : ds1
 main = goto cs0 (record {a = 100 ; b = 50})
 </code></pre>
 <pre><code>main : Meta
-main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
+main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70})
+; c' = 0 ; next = (N.cs id)})
 </code></pre>
 </div>
 <div class='slide '>
 <li>依存型をCbC に導入して自身を証明可能にする</li>
 <li>型情報から stub を自動生成すkる</li>
 <li>赤黒木の挿入に関する性質を証明する</li>
 </ul>
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-11">発表履歴</h1>
+<ul>
+<li>Agda 入門.
+<ul>
+<li>オープンソースカンファレンス 2014 Okinawa, May 2014.</li>
+</ul>
+</li>
+<li>形式手法を学び始めて思うことと、形式手法を広めるには(2p).
+<ul>
+<li>情報処理学会ソフトウェア工学研究会 (IPSJ SIGSE) ウィンターワークショップ 2015・ イン・宜野湾 (WWS2015), Jan 2015.</li>
+</ul>
+</li>
+<li>Continuation based C を用いたプログラムの検証手法(6p).
+<ul>
+<li>2016 年並列/分散/協調処理に関する『松本』サマー・ワークショップ (SWoPP2016)</li>
+<li>情報処理学会・プログラミング研究会 第 110 回プログラミング研究会 (PRO-2016-2) Aug 2016.</li>
+</ul>
+</li>
+</ul>
 <!-- vim: set filetype=markdown.slide: -->
 <!-- === end markdown block === -->
 </div>

Mercurial > hg > Papers > 2017 > atton-master

comparison presentation/slide.html @ 120:8a84cda440f3