CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 27: YAMPIIライブラリ中のポインタ操作のAgda-IVEよる検証


実施年度2007
概要 MPI通信ライブラリYAMPIIにおける待ち行列操作の信頼性を、Agda-IVEと pfvalidにより検証した。
担当者 加藤紀夫、齋藤正也
班名 対話型検証研究班
寄与 なし
関連する事例

題材

領域 通信ライブラリ
題材の詳細
YAMPIIライブラリのうち、通信を管理する待ち行列に関係する部分
形態 ソースコード
言語 C言語
規模 全体で60,000行程
題材の情報源 石川裕: YAMPII もう一つのMPI実装, 情報処理学会誌, IPSJSIG Notes 2004-HPC-099, pp.115--120, 2004

検証のデータ

目的
一般的なライブラリ利用の下で、
通信を管理する待ち行列が破壊されないことの検証。
検証内容
YAMPIIライブラリのうちの関係部分およびライブラリ利用のシナリオを
PML言語によりモデル化した。
そして、ポインタ構造で実装されている待ち行列が
破壊されないことをHoare三つ組を使って証明した。
結果
不具合や問題点は発見されなかった。
検証手法 対話型定理証明と自動検証の組合せ
モデル化法 手動
使用ツール Agda-IVE, MLAT(pfvalid)
スケジュール、
労力、時間など
12人月(実施期間は4.5か月)
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
Agda-IVEの実用問題への適用, 加藤紀夫, 第四回システム検証の科学技術シンポジウム講演論文集, 算譜科学研究速報, PS-2008-002, pp. 105-107, http://unit.aist.go.jp/cvs/tr-data/PS2008-002-revise.pdf
論文発表 投稿準備中
口頭発表 加藤紀夫: Agda-IVEの実用問題への適用, 第4回システム検証の科学シンポジウム(2007年11月5日, 名古屋大学)
知的財産
その他

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.