Mercurial > hg > Papers > 2023 > soto-master

comparison Paper/master_paper.tex @ 3:c28e8156a37b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add paper init~agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 20 Jan 2023 13:40:03 +0900
parents a72446879486
children eaef105dff41
comparison
equal deleted inserted replaced
2:0425278b683b 3:c28e8156a37b
136 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが 136 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
137 できるが，専門的な知識が多く難易度が高いという欠点がある． 137 できるが，専門的な知識が多く難易度が高いという欠点がある．
138 加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、 138 加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
139 並列処理を定理証明にて検証するには考慮する状態が多すぎる。 139 並列処理を定理証明にて検証するには考慮する状態が多すぎる。
140 そのため、並列処理はモデル検査にて検証する。 140 そのため、並列処理はモデル検査にて検証する。
141 \section{モデル検査とは}
142 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
143 \section{Gears Agdaによるモデル検査の流れ}
141 144
142 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる 145 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
143 146
144 \chapter{今後の展望} 147 \chapter{今後の展望}
145 ここまでで Gears Agda により定理証明を用いた検証と 148 ここまでで Gears Agda により定理証明を用いた検証と