@techreport{oai:ipsj.ixsq.nii.ac.jp:00217142,
 author = {岩田, 駿 and 磯部, 祥尚 and 枝廣, 正人},
 issue = {54},
 month = {Mar},
 note = {制御システムの大規模・複雑化にともない，並列化によって高速処理を可能にするメニーコアによる並列制御が注目されている．しかし，並列動作には実行順序逆転やデッドロックなど，逐次動作にはない特有の問題があり，人手による並列化は容易ではない．そこで，我々は制御システムの逐次的なモデルから，それと等価な並列制御の実行コードを自動生成するモデルベース並列化システム MBP を開発している．本論文では，MBP の並列化アルゴリズムを形式仕様記述言語 CSP で厳密に記述し，定理証明器 Isabelle を用いて，実行順序逆転やデッドロックが起こらないことを証明したことを報告する．},
 title = {モデルベース並列化アルゴリズムの定理証明器による形式検証},
 year = {2022}
}