# HG changeset patch
# User atsuki
# Date 1202903555 -32400
# Node ID 18753cb3c7034a80f7de431774b4056fa8b2ff86
# Parent  23fe35aec32b5cf5dbb06249a9c9ee3d1aa6ccf4
*** empty log message ***

diff -r 23fe35aec32b -r 18753cb3c703 paper/bibliography.tex
--- a/paper/bibliography.tex	Wed Feb 13 20:34:13 2008 +0900
+++ b/paper/bibliography.tex	Wed Feb 13 20:52:35 2008 +0900
@@ -1,6 +1,9 @@
-%\chapter*{参考文献}
-%\addcontentsline{toc}{chapter}{参考文献}
+\begin{thebibliography}{99}
+    \bibitem{bib:spin}
+	``Spin - Formal Verification''.
+	http://spinroot.com/spin/whatispin.html
 
-\begin{thebibliography}{99}
-
+    \bibitem{bib:javapathfinder}
+	``Java PathFinder''.
+	http://javapathfinder.sourceforge.net/
 \end{thebibliography}
diff -r 23fe35aec32b -r 18753cb3c703 paper/chapter2.tex
--- a/paper/chapter2.tex	Wed Feb 13 20:34:13 2008 +0900
+++ b/paper/chapter2.tex	Wed Feb 13 20:52:35 2008 +0900
@@ -232,7 +232,7 @@
 
 \subsection{SPINの概要}
 有限状態遷移系に対する形式的検査手法としてモデル検査手法がある。
-その代表的なツールとしてSPINがある。
+その代表的なツールとしてSPIN\cite{bib:spin}がある。
 
 SPINは、プログラム変換的な手法で検証するツールで、
 検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、