\documentclass[submit,techrep,noauthor]{ipsj}
%\documentclass{ipsj}

\usepackage[dvipdfmx]{graphicx}
\usepackage{latexsym}
\usepackage{listings}

\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\|{\verb|}

%\setcounter{巻数}{59}
%\setcounter{号数}{1}
%\setcounter{page}{1}
\pagestyle{empty}



%\受付{2016}{3}{4}
%\再受付{2015}{7}{16}   %省略可能
%\再再受付{2015}{7}{20} %省略可能
%\再再受付{2015}{11}{20} %省略可能
%\採録{2016}{8}{1}




\begin{document}
\bibliographystyle{ipsjunsrt} % for bibliography


\title{Gears OSのモデル検査の実装}

\etitle{Implementing Gears OS Model Checking}

%\affiliate{IPSJ}{情報処理学会\\
%IPSJ, Chiyoda, Tokyo 101--0062, Japan}


\affiliate{IE}{琉球大学工学部\\
Faculty of Engineering, University of the Ryukyus}

\author{河野 真治}{Kono Shinji}{IE}[kono@ie.u-ryukyu.ac.jp]


\begin{abstract}
\input{abstract}
\end{abstract}


\begin{jkeyword}
モデル検査, OS
\end{jkeyword}

\begin{eabstract}
Gears OS has continuation based description of user programs and the kernel. Using meta programming facility, we can
perform model checks on the user program and even the kernel itself. In this paper, we show an implmentation on 
the model checking and show the evalution.
\end{eabstract}

\begin{ekeyword}
Model checking, OS
\end{ekeyword}

\maketitle

\input 0.tex


\bibliography{ref}

\end{document}