@techreport{oai:ipsj.ixsq.nii.ac.jp:00157723,
 author = {伊達, 弘明 and 吉浦, 紀晃 and Hiroaki, Date and Yoshiura, Noriaki},
 issue = {38},
 month = {Feb},
 note = {柔軟なパケット転送を行いたいという要求により，OpenFlowが提案されている．OpenFlowスイッチの導入により大規模なネットワーク構築や構成変更をより柔軟に行えるようになった一方，OpenFlowコントローラの転送ルールをプログラミングするため，NetCore，Trema，Freneticなど様々な言語やソフトウェアが開発されてきた．これらのうち，NetCoreとは関数型言語Haskellでプログラミングできる言語であり，宣言型であること，モジュール構造を持っているなどの特徴がある．NetCoreに対する研究として，定理証明支援ソフトCoq上において，そのプログラムの健全性と完全性を証明する事が行われた．この研究により，NetCoreによりプログラミングされた言語が，プログラマの意図した通りにパケットを転送できるかを検証する事が可能となった．本稿では，イッチ同士の接続による閉路が存在するとき，NetCoreによる適切なルール設定により論理的にループを除去することが可能であるかをCoqを用いて検証した．, OpenFlow is proposed for flexible forwarding of packets. OpenFlow enables to construct and change large networks flexibly. Several programming languages such NetCore, Trema and Frenetic have been proposed for configurations of OpenFlow controllers. NetCore can be used in Haskell, which is a functional programming language. There are several features of NetCore. NetCore is a declarative programming language and has a module structure. Programming in NetCore can be verified on Coq, which is a formal proof management system. This paper uses Coq to verify NetCore programmings for networks that consist of several OpenFlow Switches. Especially, this paper focus on verification of loop-free networks.},
 title = {NetCoreプログラムのCoqによる検証},
 year = {2016}
}