--- a/paper/akasha.tex	Thu Feb 09 18:54:18 2017 +0900
+++ b/paper/akasha.tex	Thu Feb 09 18:58:53 2017 +0900
@@ -203,14 +203,14 @@
     \begin{center}
         \includegraphics[width=300pt]{fig/akashaPut.pdf}
         \caption{put を利用するプログラムのメタを上書きする}
-        \label{fig:akahsaPut}
+        \label{fig:akashaPut}
     \end{center}
 \end{figure}
 
 \verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。
-検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。
+検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続であった(リスト\ref{src:default-meta})。
 
-\lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c}
+\lstinputlisting[label=src:default-meta, caption=通常の CodeSegment の軽量継続] {src/meta.c}
 
 これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。
 検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。
@@ -227,7 +227,7 @@
 % {{{ モデル検査器 CBMC との比較
 
 \section{モデル検査器 CBMC との比較}
-akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いて赤黒木を検証した。
+akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cbmc} を用いて赤黒木を検証した。
 CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。
 
 比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文は厳密にはCとは異なるために変換が必要である。