\documentclass[12pt,a4paper,uplatex]{ujreport}
\usepackage{master_paper}
\usepackage{ascmac}
\usepackage[dvipdfmx]{graphicx}
\usepackage{here}
\usepackage{listings}
\usepackage{comment}
\usepackage{url}
\usepackage[deluxe, multi]{otf}
% 以下はハイパーリンク　要ダウンロード
\usepackage[dvipdfmx]{hyperref}
\usepackage{pxjahyper}

\usepackage{ascmac}
\usepackage[fleqn]{amsmath}
\usepackage{amssymb}

%\input{dummy.tex} %% font

\jtitle{Gears Agda での形式手法}
\etitle{Formal Methods in Gears Agda} %
\year{2023年 3月}
\eyear{March 2023}
\author{上地 悠斗}
\eauthor{Yuto Uechi}
\chife{指導教員：教授 和田 知久}
\echife{Supervisor: Prof. Tomohisa Wada}

\marklefthead{% 左上に挿入
  \begin{minipage}[b]{.4\textwidth}
    琉球大学大学院学位論文(修士)
\end{minipage}}

% \markleftfoot{% 左下に挿入
%  \begin{minipage}{.8\textwidth}
%    Gears OS の Paging
% \end{minipage}}

\newcommand\figref[1]{図 \ref{fig:#1}}
\newcommand\tabref[1]{表 \ref{tab:#1}}
\newcommand\coderef[1]{ソースコード \ref{code:#1}}

\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, 
  numbers=left,
  numberstyle={\scriptsize}, % 
  stepnumber=1, 
  numbersep=0.5zw, % 
  lineskip=-0.5ex, 
  escapechar= \! ,
}

\def\lstlistingname{ソースコード}
\def\lstlistlistingname{ソースコード目次}

% ハイパーリンク
\hypersetup{
setpagesize=false,
 bookmarksnumbered=true,%
 bookmarksopen=true,%
 colorlinks=true,%
 linkcolor=black,
 citecolor=black,
}

%%% 索引のために以下の2行を追加
%\usepackage{makeidx,multicol}
%\makeindex
\begin{document}
%rome
\maketitle
\pagenumbering{roman}
\setcounter{page}{0}
\newpage


\makecommission
%\input{chapter/signature.tex}

\newpage

%要旨
\input{tex/abst.tex}

%発表履歴
\input{tex/history.tex}
\addcontentsline{toc}{chapter}{研究関連論文業績}

\mainmatter
%目次
\tableofcontents

%図目次
\listoffigures

%表目次
% \listoftables

%リスト目次
\lstlistoflistings

%chapters
\input{tex/intro.tex}
\input{tex/cbc.tex}
\input{tex/agda.tex}

\input{tex/cbc_agda.tex}


\chapter{Gears Agda による定理証明}
\input{tex/hoare.tex}
\input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
\input{tex/tree_desc.tex}% Gears Agda における木構造の設計

\chapter{Gears Agda によるモデル検査}
モデル検査はプログラムが入力に対して仕様を満たした動作を
行うことを網羅的に検証することを指す．

モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる
状態爆発が起こり得るという問題がある．
定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
できるが，専門的な知識が多く難易度が高いという欠点がある．
加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
並列処理を定理証明にて検証するには考慮する状態が多すぎる。
そのため、並列処理はモデル検査にて検証する。
\section{モデル検査とは}
\input{tex/spin_dpp.tex}% Gears Agda の記法　loopのやつやる
\section{Gears Agdaによるモデル検査の流れ}

% Gears Agdaの場合はListの方が停止することがわかりやすいので、今回はState Listを作成した。本来はburanceされたtree structureが最も良い

\input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる

\chapter{まとめと今後の展望}
ここまでで Gears Agda により定理証明を用いた検証と
モデル検査による検証方法を確立した．
これからは Red Black Tree の定理証明を用いた検証と，
モデル検査部分では現在boundedな検知を行っているので
unboundedな検知を行えるようにしたい．

% %謝辞
\input{tex/thanks.tex}


%参考文献
\nocite{*}
\bibliography{reference}
\bibliographystyle{junsrt}


%発表履歴
%\addcontentsline{toc}{chapter}{発表履歴}
%\input{chapter/history.tex}

%付録
\addcontentsline{toc}{chapter}{付録}
\appendix
\input{tex/appendix.tex}
\end{document}