Mercurial > hg > Papers > 2023 > soto-master
comparison Paper/master_paper.tex @ 5:eaef105dff41
Add paper dpp
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 21 Jan 2023 17:57:20 +0900 |
| parents | c28e8156a37b |
| children | c821e707a5ee |
comparison
equal
deleted
inserted
replaced
| 4:4f5dde4cff0b | 5:eaef105dff41 |
|---|---|
| 16 \usepackage{amssymb} | 16 \usepackage{amssymb} |
| 17 | 17 |
| 18 %\input{dummy.tex} %% font | 18 %\input{dummy.tex} %% font |
| 19 | 19 |
| 20 \jtitle{Gears Agda での形式手法} | 20 \jtitle{Gears Agda での形式手法} |
| 21 \etitle{} % | 21 \etitle{Formal Methods in Gears Agda} % |
| 22 \year{2023年 3月} | 22 \year{2023年 3月} |
| 23 \eyear{March 2022} | 23 \eyear{March 2023} |
| 24 \author{上地 悠斗} | 24 \author{上地 悠斗} |
| 25 \eauthor{Yuto Uechi} | 25 \eauthor{Yuto Uechi} |
| 26 \chife{指導教員：教授 和田 知久} | 26 \chife{指導教員：教授 和田 知久} |
| 27 \echife{Supervisor: Prof. Tomohisa Wada} | 27 \echife{Supervisor: Prof. Tomohisa Wada} |
| 28 | 28 |
| 29 | |
| 30 \marklefthead{% 左上に挿入 | 29 \marklefthead{% 左上に挿入 |
| 31 \begin{minipage}[b]{.4\textwidth} | 30 \begin{minipage}[b]{.4\textwidth} |
| 32 琉球大学大学院学位論文(修士) | 31 琉球大学大学院学位論文(修士) |
| 33 \end{minipage}} | 32 \end{minipage}} |
| 34 | |
| 35 | 33 |
| 36 % \markleftfoot{% 左下に挿入 | 34 % \markleftfoot{% 左下に挿入 |
| 37 % \begin{minipage}{.8\textwidth} | 35 % \begin{minipage}{.8\textwidth} |
| 38 % Gears OS の Paging | 36 % Gears OS の Paging |
| 39 % \end{minipage}} | 37 % \end{minipage}} |
| 83 %\usepackage{makeidx,multicol} | 81 %\usepackage{makeidx,multicol} |
| 84 %\makeindex | 82 %\makeindex |
| 85 \begin{document} | 83 \begin{document} |
| 86 %rome | 84 %rome |
| 87 \maketitle | 85 \maketitle |
| 88 | 86 \pagenumbering{roman} |
| 87 \setcounter{page}{0} | |
| 89 \newpage | 88 \newpage |
| 90 | 89 |
| 91 \pagenumbering{roman} | 90 |
| 92 \setcounter{page}{0} | |
| 93 \makecommission | 91 \makecommission |
| 94 %\input{chapter/signature.tex} | 92 %\input{chapter/signature.tex} |
| 95 | 93 |
| 96 \newpage | 94 \newpage |
| 97 | 95 |
| 140 そのため、並列処理はモデル検査にて検証する。 | 138 そのため、並列処理はモデル検査にて検証する。 |
| 141 \section{モデル検査とは} | 139 \section{モデル検査とは} |
| 142 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない | 140 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない |
| 143 \section{Gears Agdaによるモデル検査の流れ} | 141 \section{Gears Agdaによるモデル検査の流れ} |
| 144 | 142 |
| 143 % Gears Agdaの場合はListの方が停止することがわかりやすいので、今回はState Listを作成した。本来はburanceされたtree structureが最も良い | |
| 144 | |
| 145 \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる | 145 \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる |
| 146 | 146 |
| 147 \chapter{今後の展望} | 147 \chapter{今後の展望} |
| 148 ここまでで Gears Agda により定理証明を用いた検証と | 148 ここまでで Gears Agda により定理証明を用いた検証と |
| 149 モデル検査による検証方法を確立した． | 149 モデル検査による検証方法を確立した． |