changeset 4:18753cb3c703

*** empty log message ***
author atsuki
date Wed, 13 Feb 2008 20:52:35 +0900
parents 23fe35aec32b
children db0d95f0b2e0
files paper/bibliography.tex paper/chapter2.tex
diffstat 2 files changed, 8 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- 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}
--- 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)という言語で記述し、