% withpage: ページ番号をつける (著者確認用)
% english: 英語原稿用フォーマット
\documentclass{ipsjprosym}
%\documentclass[withpage, english]{ipsjprosym}

\usepackage[dvipdfmx]{graphicx}
\usepackage{latexsym}
\usepackage{comment}
\usepackage{listings}
\usepackage{here}
\lstset{
  language=C, 
  tabsize=2, 
  frame=single, 
  basicstyle={\tt\footnotesize}, % 
  identifierstyle={\footnotesize}, % 
  commentstyle={\footnotesize\itshape}, % 
  keywordstyle={\footnotesize\ttfamily}, % 
  ndkeywordstyle={\footnotesize\ttfamily}, % 
  stringstyle={\footnotesize\ttfamily}, 
  breaklines=true, 
  captionpos=b, 
  columns=[l]{fullflexible}, % 
  xrightmargin=0zw, % 
  xleftmargin=1zw, % 
  aboveskip=1zw, 
  numberstyle={\scriptsize}, % 
  stepnumber=1, 
  numbersep=0.5zw, % 
  lineskip=-0.5ex, 
}
\renewcommand{\lstlistingname}{Code}
\usepackage{caption}
\captionsetup[lstlisting]{font={small, tt}}
\usepackage{url}
\begin{document}

% Title,  Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{継続を基本としたOS Gears OS}

%\affiliate{IPSJ}{情報処理学会}
\affiliate{KRYUKYU}{琉球大学大学院理工学研究科情報工学専攻}
\affiliate{IERYUKYU}{琉球大学工学部情報工学科}

\author{清水 隆博}{Takahiro SHIMIZU}{KRYUKYU}[anatofuz@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji KONO}{IERYUKYU}[kono@ie.u-ryukyu.ac.jp]

%概要
\begin{abstract}
継続を基本とするCと互換性のある言語、Conitinuation Based C(CbC)を用いてOSの実装を考案した。
状態遷移単位でOSの処理を実装することで、入出力が明確化され、定理証明支援系などとの表現形式と同様の表現で動作が記述可能である。
ここでは現在CbCを用いて開発しているGearsOSについての実装及び今後の展望について考察する。
\end{abstract}

\begin{jkeyword}
システムプログラミング, CbC, 軽量継続, OS
\end{jkeyword}

\maketitle

% Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{証明可能なOS}
コンピュータ上で動作するあらゆるソフトウェアや資源を管理するOSは、 高い信頼性が保証されるべきである。
信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。
現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。



\nocite{*}
\bibliographystyle{ipsjsort}
\bibliography{reference}

\end{document}