Mercurial > hg > Papers > 2023 > soto-master
diff Paper/master_paper.tex @ 3:c28e8156a37b
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 |
line wrap: on
line diff
--- a/Paper/master_paper.tex Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/master_paper.tex Fri Jan 20 13:40:03 2023 +0900 @@ -138,6 +138,9 @@ 加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、 並列処理を定理証明にて検証するには考慮する状態が多すぎる。 そのため、並列処理はモデル検査にて検証する。 +\section{モデル検査とは} +\section{SPINによるモデル検査}% 内容にそぐわない場合は使わない +\section{Gears Agdaによるモデル検査の流れ} \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる