項書換え系と木オートマトンに基づくプログラム安全性検証に関する研究

2010 年度 自己評価報告書

• 研究課題/領域番号: 20300010
• 研究種目: 基盤研究(B)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 名古屋大学
• 研究代表者: 坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829)
• 研究期間 (年度): 2008 – 2011
• キーワード: 仕様記述 / 仕様検証

研究概要

本研究の目的は,項書換え系や木オートマトンの解析技法を応用し,通信プロトコルを始めとするネットワークソフトウエアを含む並行プログラム一般の安全性について,効率的かつ適用範囲の広い検証技法を確立するとともに,検証システムを実装,評価することである
本課題では,以下の項目を研究する計画である
(1)応用pi計算における弱い非干渉性の定式化
(2)応用pi計算における安全型の定式化
(3)安全型と弱い非干渉性の関係の解明
(4)項書換え系と木オートマトンに基づいた安全型の近似型推論システムの開発
(5)近似型推論システムへの応用に特化された項書換え系と木オートマトンの解析技法の開発
(6)近似型推論システムに基づく安全性検証システムの実装と実験による評価

研究成果

• [雑誌論文] 制約付き項書換え系の書換え帰納法における補題等式の自動生成法 (2011)
  • 著者名/発表者名: 中林直生, 西田直樹, 草刈圭一朗, 坂部俊樹, 酒井正彦
  • 雑誌名: コンピュータソフトウェア 28 ページ: 173-189
  • 査読あり
• [雑誌論文] 等式理論を法とするDPLL遷移系について (2010)
  • 著者名/発表者名: 馬場達也, 坂部俊樹, 西田直樹, 草刈圭一朗, 酒井正彦
  • 雑誌名: 電子情報通信学会ソフトウェアサイエンス研究会 SS2010-36 ページ: 49-54
• [雑誌論文] 基本対称関数に基づく節をもつCNF論理式の充足可能性判定 (2010)
  • 著者名/発表者名: 馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗
  • 雑誌名: 電子情報通信学会論文誌D J93-D ページ: 1-9
  • 査読あり
• [雑誌論文] Decidability of Termination and Innermost Termination for Term Rewriting S ystems with Right-Shallow Dependency Pairs (2010)
  • 著者名/発表者名: Keita Uchiyam, Masahiko Sakai, Toshiki Sakabe
  • 雑誌名: IEICE Trans. on Information and Systems E93-D ページ: 953-962
  • 査読あり
• [雑誌論文] 制約付き項書換え系における書換え帰納法 (2009)
  • 著者名/発表者名: 坂田翼, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一郎
  • 雑誌名: 情報処理学会論文誌プログラミング 2 ページ: 80-96
  • 査読あり
• [雑誌論文] ビットエラー通信路におけるスケーラブルCANの動作解析 (2008)
  • 著者名/発表者名: 鵜飼謙児, 坂部俊樹, 高田広章, 倉地亮, 酒井正彦, 草刈圭一朗, 西田直樹
  • 雑誌名: 電子情報通信学会技術研究報告(SS2008-37) 108 ページ: 61-66