Mercurial > hg > Papers > 2016 > atton-ipsjpro

changeset 64:f5cad08f76b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slide for presentation
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 10 Aug 2016 15:10:07 +0900
parents 60faf7f9d741
children c73e1ee2d5ee
files paper/vmpcbc.pdf paper/vmpcbc.tex presentation/slide.html presentation/slide.md presentation/slide.pdf.html
diffstat 5 files changed, 117 insertions(+), 381 deletions(-) [+]
line wrap: on
line diff
Binary file paper/vmpcbc.pdf has changed
--- a/paper/vmpcbc.tex	Mon Aug 08 22:11:48 2016 +0900
+++ b/paper/vmpcbc.tex	Wed Aug 10 15:10:07 2016 +0900
@@ -620,356 +620,6 @@
 
 \end{thebibliography}
 
-\appendix
-
-% {{{ CbCで記述された赤黒木のコード
-
-\section{CbCで記述された赤黒木のコード}
-CbCで記述された赤黒木のソースコードを図\ref{src:rbtree-full} に示す。
-
-
-\begin{lstlisting}[ caption={CbCで記述された赤黒木}, label=src:rbtree-full  ]
-enum Relational {
-    EQ,
-    GT,
-    LT,
-};
-
-enum UniqueData {
-    Allocate,
-    Tree,
-    Node,
-};
-
-struct Context {
-    enum Code next;
-    int codeNum;
-    __code (**code) (struct Context*);
-    void* heapStart;
-    void* heap;
-    long heapLimit;
-    int dataNum;
-    stack_ptr code_stack;
-    stack_ptr node_stack;
-    union Data **data;
-};
-
-union Data {
-    struct Comparable { // inteface
-        enum Code compare;
-        union Data* data;
-    } compare;
-    struct Count {
-        enum Code next;
-        long i;
-    } count;
-    struct Tree {
-        enum Code next;
-        struct Node* root;
-        struct Node* current;
-        struct Node* deleted;
-        int result;
-    } tree;
-    struct Node {
-        // need to tree
-        enum Code next;
-        int key; // comparable data segment
-        int value;
-        struct Node* left;
-        struct Node* right;
-        // need to balancing
-        enum Color {
-            Red,
-            Black,
-        } color;
-    } node;
-    struct Allocate {
-        enum Code next;
-        long size;
-    } allocate;
-};
-
-
-__code put(struct Context* context, struct Tree* tree, struct Node* root, struct Allocate* allocate) {
-    allocate->size = sizeof(struct Node);
-    allocator(context);
-
-    stack_push(context->code_stack, &context->next);
-
-    context->next = StackClear;
-    stack_push(context->code_stack, &context->next);
-
-    tree->root = &context->data[context->dataNum]->node;
-
-    if (root) {
-        tree->current = root;
-        compare(context, tree, tree->current->key, context->data[Node]->node.key);
-
-        goto meta(context, Replace);
-    }
-
-    goto meta(context, Insert);
-}
-
-__code put_stub(struct Context* context) {
-    goto put(context, &context->data[Tree]->tree, context->data[Tree]->tree.root, &context->data[Allocate]->allocate);
-}
-
-__code replaceNode(struct Context* context, struct Tree* tree, struct Node* oldNode, struct Node* newNode, int result) {
-    *newNode = *oldNode;
-    stack_push(context->node_stack, &newNode);
-
-    if (result == EQ) {
-        newNode->value = context->data[Node]->node.value;
-
-        stack_pop(context->code_stack, &context->next);
-        goto meta(context, context->next);
-    } else if (result == GT) {
-        tree->current = oldNode->right;
-        newNode->right = context->heap;
-    } else {
-        tree->current = oldNode->left;
-        newNode->left = context->heap;
-    }
-
-    context->data[Allocate]->allocate.size = sizeof(struct Node);
-    allocator(context);
-
-    if (tree->current) {
-        compare(context, tree, tree->current->key, context->data[Node]->node.key);
-        goto meta(context, Replace);
-    }
-
-    goto meta(context, Insert);
-}
-
-__code replaceNode_stub(struct Context* context) {
-    goto replaceNode(context, &context->data[Tree]->tree, context->data[Tree]->tree.current, &context->data[context->dataNum]->node, context->data[Tree]->tree.result);
-}
-
-__code insertNode(struct Context* context, struct Tree* tree, struct Node* node, struct Node* newNode) {
-    node->color = Red;
-    *newNode = *node;
-
-    tree->current = newNode;
-
-    goto meta(context, InsertCase1);
-}
-
-__code insertNode_stub(struct Context* context) {
-    goto insertNode(context, &context->data[Tree]->tree, &context->data[Node]->node, &context->data[context->dataNum]->node);
-}
-
-__code insertCase1(struct Context* context, struct Tree* tree, struct Node* current) {
-    if (!isEmpty(context->node_stack))
-        goto meta(context, InsertCase2);
-
-    tree->root->color = Black;
-
-    stack_pop(context->code_stack, &context->next);
-    goto meta(context, context->next);
-}
-
-__code insert1_stub(struct Context* context) {
-    goto insertCase1(context, &context->data[Tree]->tree, context->data[Tree]->tree.current);
-}
-
-__code insertCase2(struct Context* context, struct Node* current) {
-    struct Node* parent;
-    stack_pop(context->node_stack, &parent);
-
-    if (parent->color == Black) {
-        stack_pop(context->code_stack, &context->next);
-        goto meta(context, context->next);
-    }
-
-    stack_push(context->node_stack, &parent);
-    goto meta(context, InsertCase3);
-}
-
-__code insert2_stub(struct Context* context) {
-    goto insertCase2(context, context->data[Tree]->tree.current);
-}
-
-__code insertCase3(struct Context* context, struct Tree* tree, struct Node* current) {
-    struct Node* parent;
-    struct Node* uncle;
-    struct Node* grandparent;
-
-    stack_pop(context->node_stack, &parent);
-    stack_pop(context->node_stack, &grandparent);
-
-    if (grandparent->left == parent)
-        uncle = grandparent->right;
-    else
-        uncle = grandparent->left;
-
-    if (uncle && (uncle->color == Red)) {
-        parent->color = Black;
-        uncle->color = Black;
-        grandparent->color = Red;
-        tree->current = grandparent;
-        goto meta(context, InsertCase1);
-    }
-
-    stack_push(context->node_stack, &grandparent);
-    stack_push(context->node_stack, &parent);
-
-    goto meta(context, InsertCase4);
-}
-
-__code insert3_stub(struct Context* context) {
-    goto insertCase3(context, &context->data[Tree]->tree, context->data[Tree]->tree.current);
-}
-
-__code insertCase4(struct Context* context, struct Tree* tree, struct Node* current) {
-    struct Node* parent;
-    struct Node* grandparent;
-
-    stack_pop(context->node_stack, &parent);
-    stack_pop(context->node_stack, &grandparent);
-
-    stack_push(context->node_stack, &grandparent);
-
-    tree->current = parent;
-
-    if ((current == parent->right) && (parent == grandparent->left)) {
-        context->next = InsertCase4_1;
-
-        stack_push(context->code_stack, &context->next);
-        goto meta(context, RotateL);
-    } else if ((current == parent->left) && (parent == grandparent->right)) {
-        context->next = InsertCase4_2;
-
-        stack_push(context->code_stack, &context->next);
-        goto meta(context, RotateR);
-    }
-
-    stack_push(context->node_stack, &parent);
-    tree->current = current;
-    goto meta(context, InsertCase5);
-}
-
-__code insert4_stub(struct Context* context) {
-    goto insertCase4(context, &context->data[Tree]->tree, context->data[Tree]->tree.current);
-}
-
-__code insertCase4_1(struct Context* context, struct Tree* tree) {
-    stack_push(context->node_stack, &tree->current);
-    tree->current = tree->current->left;
-    goto meta(context, InsertCase5);
-}
-
-__code insert4_1_stub(struct Context* context) {
-    goto insertCase4_1(context, &context->data[Tree]->tree);
-}
-
-__code insertCase4_2(struct Context* context, struct Tree* tree) {
-    stack_push(context->node_stack, &tree->current);
-    tree->current = tree->current->right;
-    goto meta(context, InsertCase5);
-}
-
-__code insert4_2_stub(struct Context* context) {
-    goto insertCase4_2(context, &context->data[Tree]->tree);
-}
-
-__code insertCase5(struct Context* context, struct Tree* tree, struct Node* current) {
-    struct Node* parent;
-    struct Node* grandparent;
-
-    stack_pop(context->node_stack, &parent);
-    stack_pop(context->node_stack, &grandparent);
-
-    parent->color = Black;
-    grandparent->color = Red;
-
-    tree->current = grandparent;
-
-    if ((current == parent->left) && (parent == grandparent->left))
-        goto meta(context, RotateR);
-    else
-        goto meta(context, RotateL);
-}
-
-__code insert5_stub(struct Context* context) {
-    goto insertCase5(context, &context->data[Tree]->tree, context->data[Tree]->tree.current);
-}
-
-__code rotateLeft(struct Context* context, struct Node* node, struct Tree* tree) {
-    struct Node* tmp = node->right;
-    struct Node* parent = 0;
-
-    stack_pop(context->node_stack, &parent);
-
-    if (parent) {
-        if (node == parent->left)
-            parent->left = tmp;
-        else
-            parent->right = tmp;
-    } else {
-        tree->root = tmp;
-    }
-
-    stack_push(context->node_stack, &parent);
-
-    node->right = tmp->left;
-    tmp->left = node;
-    tree->current = tmp;
-
-    stack_pop(context->code_stack, &context->next);
-    goto meta(context, context->next);
-}
-
-__code rotateLeft_stub(struct Context* context) {
-    goto rotateLeft(context, context->data[Tree]->tree.current, &context->data[Tree]->tree);
-}
-
-__code rotateRight(struct Context* context, struct Node* node, struct Tree* tree) {
-    struct Node* tmp = node->left;
-    struct Node* parent = 0;
-
-    stack_pop(context->node_stack, &parent);
-
-    if (parent) {
-        if (node == parent->left)
-            parent->left = tmp;
-        else
-            parent->right = tmp;
-    } else {
-        tree->root = tmp;
-    }
-
-    stack_push(context->node_stack, &parent);
-
-    node->left = tmp->right;
-    tmp->right = node;
-    tree->current = tmp;
-
-    stack_pop(context->code_stack, &context->next);
-    goto meta(context, context->next);
-}
-
-__code rotateRight_stub(struct Context* context) {
-    goto rotateRight(context, context->data[Tree]->tree.current, &context->data[Tree]->tree);
-}
-
-__code stackClear(struct Context* context, stack_ptr node_stack, struct Tree* tree) {
-    if (stack_pop(node_stack, &tree->current) == 0)
-        goto meta(context, StackClear);
-
-    tree->current = 0;
-
-    stack_pop(context->code_stack, &context->next);
-    goto meta(context, context->next);
-}
-
-__code stackClear_stub(struct Context* context) {
-    goto stackClear(context, context->node_stack, &context->data[Tree]->tree);
-}
-\end{lstlisting}
-
-% }}}
 
 \begin{biography}
 \profile{n}{比嘉健太}{1992年生。2015年琉球大学工学部情報工学科卒業。2015年琉球大学大学院理工学研究科情報工学専攻入学。}
--- a/presentation/slide.html	Mon Aug 08 22:11:48 2016 +0900
+++ b/presentation/slide.html	Wed Aug 10 15:10:07 2016 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.0 (2015-12-25) [x86_64-darwin14]
-                on 2016-08-08 09:27:07 +0900 with Markdown engine kramdown (1.9.0)
+                on 2016-08-10 12:46:48 +0900 with Markdown engine kramdown (1.9.0)
                   using options {}
   -->
 
@@ -116,12 +116,12 @@
     <ul>
       <li>Java Path Finder
         <ul>
-          <li>JVM を切り替える</li>
+          <li>JVM を切り替えてスレッドの実行順番を列挙</li>
         </ul>
       </li>
       <li>Valgrind
         <ul>
-          <li>バイナリを動的解析</li>
+          <li>バイナリを動的解析してメモリリークを検出</li>
         </ul>
       </li>
       <li>大規模システムは実行できない</li>
@@ -137,7 +137,7 @@
 <ul>
   <li>アルゴリズムの正しさを証明する
     <ul>
-      <li>Agda, Coq, Idris といった証明支援系でアルゴリズムを記述する</li>
+      <li>Agda, Coq といった証明支援系でアルゴリズムを記述する</li>
       <li>極めて難しい</li>
       <li>実装に対して適用できない</li>
     </ul>
@@ -205,6 +205,7 @@
 <ul>
   <li>Code Segment は <code>__code</code> を付けた関数</li>
   <li>次の Code Segment への接続は <code>goto</code> で表される</li>
+  <li>Data Segment は構造体</li>
 </ul>
 
 <pre><code>__code addTen(struct Count c) {
@@ -264,7 +265,7 @@
 <!-- _S9SLIDE_ -->
 <h1 id="cbc--2">CbC のメタ計算の実際</h1>
 <ul>
-  <li>メタ計算レベルでは Data Segment は union Data という形で一様</li>
+  <li>メタ計算レベルでは Data Segment は union Data という形で一様に扱う</li>
   <li>メタ計算と通常の計算は stub と meta によって接続される
     <ul>
       <li>stub では利用する Data Segment の指定などを行なう</li>
@@ -391,7 +392,7 @@
   </li>
   <li>CbC のメタ計算 Akasha では要素数13個までチェックできた
     <ul>
-      <li>13の階乗で62億通りを1,2時間ほど</li>
+      <li>13の階乗の62億通りを8時間ほど</li>
     </ul>
   </li>
   <li>実装にわざとバグを入れた場合にはバランスしない入力例を返した</li>
@@ -401,6 +402,31 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="akasha--1">Akasha による赤黒木の検証方法</h1>
+<ul>
+  <li>挿入される可能性のある全ての要素を持つ循環リストを作成</li>
+  <li>木に対して要素を1つ挿入する
+    <ul>
+      <li>挿入した要素を排除した循環リストを作成</li>
+      <li>挿入後に作成された木を保存する</li>
+      <li>挿入後の木がバランスされているかをチェックする</li>
+      <li>反例用に挿入した要素を記録</li>
+    </ul>
+  </li>
+  <li>全ての要素を挿入したら
+    <ul>
+      <li>保存していた木と循環リストを再現して深さを高くする</li>
+      <li>循環リストの head を1つ進める</li>
+      <li>循環リストの head と tail が同じになったら深さを高くする</li>
+    </ul>
+  </li>
+  <li>最初の循環リストの head と tail が同じになったら終了</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="c-bounded-model-checker">C Bounded Model Checker</h1>
 <ul>
   <li>Carnegie Mellon University で開発されている記号実行モデルチェッカ
@@ -416,7 +442,7 @@
   <li>挿入順番は非決定的な入力 <code>nondet_int</code> を使う</li>
   <li>関数呼び出しやループは展開される
     <ul>
-      <li>展開可能な最大数まで展開しても赤黒木の仕様を検証できず</li>
+      <li>展開可能な最大数まで展開した時、バグを含んだ赤黒木の仕様を検証できず</li>
     </ul>
   </li>
 </ul>
@@ -459,7 +485,21 @@
   <li>挿入だけでなく削除を含む赤黒木の仕様検証</li>
   <li>ポインタへの不正アクセス検出などの機能</li>
   <li>検証用APIを CbC コンパイラに導入</li>
-  <li>CBMC 側で検証できるよう赤黒木を書き換えて検証する</li>
+  <li>CBMC 側での赤黒木検証を検討する</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="akasha-execution-environment">Akasha Execution Environment</h1>
+<ul>
+  <li>Intel(R) Xeon(R) CPU E5-2699 v3 @ 2.30GHz 18 core</li>
+  <li>メモリ: 768G</li>
+  <li>Compile Option: -O0</li>
+  <li>要素数10個: 11sec (362万通り)</li>
+  <li>要素数11個: 136sec (3991万通り)</li>
+  <li>要素数12個: 1554sec (4億7900万通り)</li>
 </ul>
 
 
@@ -471,14 +511,13 @@
   <li>CBMC 5.4</li>
   <li>実行オプション
     <ul>
-      <li>cbmc –unwind 1</li>
       <li>cbmc –depth 400 –property verifySpecification.assertion.1</li>
     </ul>
   </li>
   <li>赤黒木のCbC実装
     <ul>
       <li>赤黒木部分のみ: 330行</li>
-      <li>スタックやメモリのアロケータなどを含める: 640行</li>
+      <li>スタックやメモリのアロケータなどを含む: 640行</li>
     </ul>
   </li>
 </ul>
@@ -537,7 +576,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="akasha--1">Akasha の検証コード例</h1>
+<h1 id="akasha--2">Akasha の検証コード例</h1>
 
 <pre><code>__code verifySpecificationFinish(struct Context* context) {
     if (context-&gt;data[AkashaInfo]-&gt;akashaInfo.maxHeight &gt;
--- a/presentation/slide.md	Mon Aug 08 22:11:48 2016 +0900
+++ b/presentation/slide.md	Wed Aug 10 15:10:07 2016 +0900
@@ -16,14 +16,14 @@
     * ユニットテストと組み合わせて使う
 * 検証の計算システムで実行する(メタ計算)
     * Java Path Finder
-        * JVM を切り替える
+        * JVM を切り替えてスレッドの実行順番を列挙
     * Valgrind
-        * バイナリを動的解析
+        * バイナリを動的解析してメモリリークを検出
     * 大規模システムは実行できない
 
 # ソフトウェアの信頼性向上手法
 * アルゴリズムの正しさを証明する
-    * Agda, Coq, Idris といった証明支援系でアルゴリズムを記述する
+    * Agda, Coq といった証明支援系でアルゴリズムを記述する
     * 極めて難しい
     * 実装に対して適用できない
 * ソフトウェアの仕様を記述し、その反例が無いかをチェックする
@@ -57,6 +57,7 @@
 # Example of Code Segment in CbC
 * Code Segment は `__code` を付けた関数
 * 次の Code Segment への接続は `goto` で表される
+* Data Segment は構造体
 
 ```
 __code addTen(struct Count c) {
@@ -99,7 +100,7 @@
 ```
 
 # CbC のメタ計算の実際
-* メタ計算レベルでは Data Segment は union Data という形で一様
+* メタ計算レベルでは Data Segment は union Data という形で一様に扱う
 * メタ計算と通常の計算は stub と meta によって接続される
     * stub では利用する Data Segment の指定などを行なう
 
@@ -178,7 +179,7 @@
     * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
     * 挿入後の木はきちんとバランスしているかチェックする
 * CbC のメタ計算 Akasha では要素数13個までチェックできた
-    * 13の階乗の62億通りを1,2時間ほど
+    * 13の階乗の62億通りを8時間ほど
 * 実装にわざとバグを入れた場合にはバランスしない入力例を返した
 
 # Akasha による赤黒木の検証方法
@@ -201,7 +202,7 @@
     * 赤黒木のコードを機械的に置換で C に変換して検証
 * 挿入順番は非決定的な入力 `nondet_int` を使う
 * 関数呼び出しやループは展開される
-    * 展開可能な最大数まで展開しても赤黒木の仕様を検証できず
+    * 展開可能な最大数まで展開した時、バグを含んだ赤黒木の仕様を検証できず
 
 # Conclusion
 * 動作するプログラムの記述を変更せず検証を行なえた
@@ -218,16 +219,23 @@
 * 挿入だけでなく削除を含む赤黒木の仕様検証
 * ポインタへの不正アクセス検出などの機能
 * 検証用APIを CbC コンパイラに導入
-* CBMC 側で検証できるよう赤黒木を書き換えて検証する
+* CBMC 側での赤黒木検証を検討する
+
+# Akasha Execution Environment
+* Intel(R) Xeon(R) CPU E5-2699 v3 @ 2.30GHz 18 core
+* メモリ: 768G
+* Compile Option: -O0
+* 要素数10個: 11sec (362万通り)
+* 要素数11個: 136sec (3991万通り)
+* 要素数12個: 1554sec (4億7900万通り)
 
 # CBMC Informations
 * CBMC 5.4
 * 実行オプション
-    * cbmc --unwind 1
     * cbmc --depth 400 --property verifySpecification.assertion.1
 * 赤黒木のCbC実装
     * 赤黒木部分のみ: 330行
-    * スタックやメモリのアロケータなどを含める: 640行
+    * スタックやメモリのアロケータなどを含む: 640行
 
 # 他の言語でのメタ計算
 * 計算を実現するような計算
--- a/presentation/slide.pdf.html	Mon Aug 08 22:11:48 2016 +0900
+++ b/presentation/slide.pdf.html	Wed Aug 10 15:10:07 2016 +0900
@@ -70,7 +70,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.0 (2015-12-25) [x86_64-darwin14]
-                on 2016-08-08 09:27:07 +0900 with Markdown engine kramdown (1.9.0)
+                on 2016-08-10 12:46:48 +0900 with Markdown engine kramdown (1.9.0)
                   using options {}
   -->
 
@@ -100,12 +100,12 @@
     <ul>
       <li>Java Path Finder
         <ul>
-          <li>JVM を切り替える</li>
+          <li>JVM を切り替えてスレッドの実行順番を列挙</li>
         </ul>
       </li>
       <li>Valgrind
         <ul>
-          <li>バイナリを動的解析</li>
+          <li>バイナリを動的解析してメモリリークを検出</li>
         </ul>
       </li>
       <li>大規模システムは実行できない</li>
@@ -121,7 +121,7 @@
 <ul>
   <li>アルゴリズムの正しさを証明する
     <ul>
-      <li>Agda, Coq, Idris といった証明支援系でアルゴリズムを記述する</li>
+      <li>Agda, Coq といった証明支援系でアルゴリズムを記述する</li>
       <li>極めて難しい</li>
       <li>実装に対して適用できない</li>
     </ul>
@@ -189,6 +189,7 @@
 <ul>
   <li>Code Segment は <code>__code</code> を付けた関数</li>
   <li>次の Code Segment への接続は <code>goto</code> で表される</li>
+  <li>Data Segment は構造体</li>
 </ul>
 
 <pre><code>__code addTen(struct Count c) {
@@ -248,7 +249,7 @@
 <!-- _S9SLIDE_ -->
 <h1 id="cbc--2">CbC のメタ計算の実際</h1>
 <ul>
-  <li>メタ計算レベルでは Data Segment は union Data という形で一様</li>
+  <li>メタ計算レベルでは Data Segment は union Data という形で一様に扱う</li>
   <li>メタ計算と通常の計算は stub と meta によって接続される
     <ul>
       <li>stub では利用する Data Segment の指定などを行なう</li>
@@ -375,7 +376,7 @@
   </li>
   <li>CbC のメタ計算 Akasha では要素数13個までチェックできた
     <ul>
-      <li>13の階乗で62億通りを1,2時間ほど</li>
+      <li>13の階乗の62億通りを8時間ほど</li>
     </ul>
   </li>
   <li>実装にわざとバグを入れた場合にはバランスしない入力例を返した</li>
@@ -385,6 +386,31 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="akasha--1">Akasha による赤黒木の検証方法</h1>
+<ul>
+  <li>挿入される可能性のある全ての要素を持つ循環リストを作成</li>
+  <li>木に対して要素を1つ挿入する
+    <ul>
+      <li>挿入した要素を排除した循環リストを作成</li>
+      <li>挿入後に作成された木を保存する</li>
+      <li>挿入後の木がバランスされているかをチェックする</li>
+      <li>反例用に挿入した要素を記録</li>
+    </ul>
+  </li>
+  <li>全ての要素を挿入したら
+    <ul>
+      <li>保存していた木と循環リストを再現して深さを高くする</li>
+      <li>循環リストの head を1つ進める</li>
+      <li>循環リストの head と tail が同じになったら深さを高くする</li>
+    </ul>
+  </li>
+  <li>最初の循環リストの head と tail が同じになったら終了</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="c-bounded-model-checker">C Bounded Model Checker</h1>
 <ul>
   <li>Carnegie Mellon University で開発されている記号実行モデルチェッカ
@@ -400,7 +426,7 @@
   <li>挿入順番は非決定的な入力 <code>nondet_int</code> を使う</li>
   <li>関数呼び出しやループは展開される
     <ul>
-      <li>展開可能な最大数まで展開しても赤黒木の仕様を検証できず</li>
+      <li>展開可能な最大数まで展開した時、バグを含んだ赤黒木の仕様を検証できず</li>
     </ul>
   </li>
 </ul>
@@ -443,7 +469,21 @@
   <li>挿入だけでなく削除を含む赤黒木の仕様検証</li>
   <li>ポインタへの不正アクセス検出などの機能</li>
   <li>検証用APIを CbC コンパイラに導入</li>
-  <li>CBMC 側で検証できるよう赤黒木を書き換えて検証する</li>
+  <li>CBMC 側での赤黒木検証を検討する</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="akasha-execution-environment">Akasha Execution Environment</h1>
+<ul>
+  <li>Intel(R) Xeon(R) CPU E5-2699 v3 @ 2.30GHz 18 core</li>
+  <li>メモリ: 768G</li>
+  <li>Compile Option: -O0</li>
+  <li>要素数10個: 11sec (362万通り)</li>
+  <li>要素数11個: 136sec (3991万通り)</li>
+  <li>要素数12個: 1554sec (4億7900万通り)</li>
 </ul>
 
 
@@ -455,14 +495,13 @@
   <li>CBMC 5.4</li>
   <li>実行オプション
     <ul>
-      <li>cbmc –unwind 1</li>
       <li>cbmc –depth 400 –property verifySpecification.assertion.1</li>
     </ul>
   </li>
   <li>赤黒木のCbC実装
     <ul>
       <li>赤黒木部分のみ: 330行</li>
-      <li>スタックやメモリのアロケータなどを含める: 640行</li>
+      <li>スタックやメモリのアロケータなどを含む: 640行</li>
     </ul>
   </li>
 </ul>
@@ -521,7 +560,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="akasha--1">Akasha の検証コード例</h1>
+<h1 id="akasha--2">Akasha の検証コード例</h1>
 
 <pre><code>__code verifySpecificationFinish(struct Context* context) {
     if (context-&gt;data[AkashaInfo]-&gt;akashaInfo.maxHeight &gt;