\documentclass[twocolumn, a4j, twoside]{jarticle}
\usepackage{master_proc}
\usepackage[dvips]{graphicx}

% dvipdfm を使って PDF ファイルに日本語の栞をつける
% \usepackage[dvipdfm]{color}
% \usepackage[dvipdfm,bookmarks=true,bookmarksnumbered=true,%
% bookmarkstype=toc]{hyperref}

\jtitle{線形時相論理によるContinuation based Cプログラムの検証}		%和文タイトル
\etitle{Verification of Continuation based C Program using Linear-time Temporal Logic}	%英文タイトル
\author{下地 篤樹}	%著者名
\studentid{068507B}	%学籍番号
\teacher{河野 真治}	%指導教官

\begin{document}
\maketitle
\section{はじめに}
リアルタイムプログラムや並列プログラムのような非決定性を含むプログラムは、
逐次型のプログラムに有効な二分法などによるデバッグ手法ではデバッグすることが
困難である。
そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
確立が重要な課題となっている。

そこで、本研究では、Continuation based C(CbC)言語による実装と
その実装に対する検証手法を提案している。
CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。

本研究は、CbCプログラムが状態遷移記述になることに着目し、
状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用さ
れる。

{\small
\begin{thebibliography}{9}
    \bibitem{bib:jssst2000kono}
	河野真治. ``継続を持つCの下位言語によるシステム記述''.
	日本ソフトウェア科学会第17回大会, 2000.
    \bibitem{bib:sigos2007}
	下地篤樹, 河野真治. ``線形時相論理によるContinuation based Cプログラムの検証''.
	情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), April, 2007.
\end{thebibliography}
}
\end{document}