CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 17: Deutsch-Schorr-WaiteマーキングアルゴリズムのAgda-MLAT連携による検証


実施年度2007, 2008
概要 Deutsch-Schorr-Waiteマーキングアルゴリズムの安全性を,Agda-MLAT連携に よって検証した.
担当者 湯浅能史,田辺良則,関澤俊弦,高橋孝一
班名 抽象化ツール研究開発班
寄与
関連する事例 事例 19:リスト反転アルゴリズムのAgda-MLAT連携による検証

題材

領域 アルゴリズム
題材の詳細
Deutsch-Schorr-Waiteマーキングアルゴリズム
形態 アルゴリズム
言語 PML, agda
規模 12000行
題材の情報源 H. Schorr, W. M. Waite: An efficient machine-independent procedure for garbage collection in various list structures. Communications of the ACM archive, Volume 10 , Issue 8 (August 1967) pp. 501 - 506 (1967)

検証のデータ

目的
新たに開発した様相μ計算充足可能性判定アルゴリズムが,実用上十分な性能を
持っていることを確認すること.
検証内容
安全性 (マークが行われること.ポインタが実行前と実行後で変化しないこと)
結果
妥当な時間内で上記の検証が行えることを確認した.
検証手法 対話型検証と自動検証の併用
モデル化法
使用ツール agda, MLAT(pfvalid)
スケジュール、
労力、時間など
1ヶ月程度
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表 Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, and Koichi Takahashi: "Verification of the Deutsh-Schorr-Waite marking algorithm with Modal Logic" Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), Lecture Notes in Computer Science, Vol. 5295, pp. 115-129, Springer, October 2008. (Tronto, Canada)
口頭発表 湯浅 能史,田辺 良則,関澤 俊弦,高橋 孝一 「Agda-MLAT連携による Schorr-Waiteマーキングアルゴリズムの検証」, 日本ソフトウェア科学会第24回 大会ポスター発表
知的財産
その他

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