無限項を扱うプログラム変換を用いたソフトウェア検証方法の研究

• 研究課題/領域番号: 24500171
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: 知能情報学
• 研究機関: 名古屋工業大学
• 研究代表者: 世木 博久 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
• 研究期間 (年度): 2012-04-01 – 2016-03-31
• 研究課題ステータス: 完了 (2015年度)
• 配分額: 4,810千円 (直接経費: 3,700千円、間接経費: 1,110千円); 2014年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円); 2013年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円); 2012年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
• キーワード: 探索・論理・推論アルゴリズム / 計算論理 / プログラム推論 / プログラム変換 / システム検証

研究成果の概要

本研究は，リアクティブ・システム等のソフトウェアの正当性を形式的に検証するための方法論の構築を目的とする．そのために，計算論理に基づく形式手法である論理プログラムに対するプログラム推論を用いるアプローチを採用し，次のような3つの主な研究成果を得た．(1) 余論理プログラムに対するプログラム推論とそれを用いた仕様の検証法を示した．(2) その結果を拡張し，ソフトウェアの正当性検証問題であるCTL時間論理式に対するモデル検査を実現できることを示した． (3) 検証に必要となるプログラムの仕様を効率的に発見するための基礎となるパターン・マイニング方法を示した．

研究成果

• [雑誌論文] Distributed Mining of Closed Patterns from Multi-Relational Data (2015)
  • 著者名/発表者名: Yohei Kamiya, Hirohisa Seki
  • 雑誌名: Journal of Advanced Computational Intelligence and Intelligent Informatics 巻: 19 ページ: 804-809
  • NAID: 130007673331
  • 査読あり / 謝辞記載あり
• [雑誌論文] Extending Co-logic Programs for Branching-Time Model Checking (2014)
  • 著者名/発表者名: Hirohisa Seki
  • 雑誌名: Lecture Notes in Computer Science 巻: 8901 ページ: 127-144
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] Proving Properties of Co-logic Programs with Negation by Program Transformations (2013)
  • 著者名/発表者名: 世木 博久
  • 雑誌名: Lecture Notes in Computer Science 巻: 7844 ページ: 213-227
  • 査読あり
• [雑誌論文] Proving Properties of Co-logic Programs by Unfold/Fold Transformations (2012)
  • 著者名/発表者名: 世木 博久
  • 雑誌名: Lecture Notes in Computer Science 巻: 7225 ページ: 205-220
  • 査読あり
• [学会発表] 関係データからの飽和パターンマイニングにおける並列化のための負荷分散方式 (2015)
  • 著者名/発表者名: 長尾 雅弘 世木 博久
  • 学会等名: 電気・電子・情報関係学会 東海支部連合大会
  • 発表場所: 名古屋工業大学
  • 年月日: 2015-09-28
• [学会発表] Towards Efficient Closed Pattern Mining from Distributed Multi-Relational Data (2014)
  • 著者名/発表者名: Yohei Kamiya, Hirohisa Seki
  • 学会等名: Joint 7th Int’l. Conf. on Soft Computing and Intelligent Systems and 15th Int’l Symp. on Advanced Intelligent Systems (SCIS&ISIS 2014)
  • 発表場所: 北九州国際会議場 (福岡県・北九州市)
  • 年月日: 2014-12-05
• [学会発表] Merging Closed Pattern Sets in Distributed Multi-Relational Data (2014)
  • 著者名/発表者名: Hirohisa Seki, Yohei Kamiya
  • 学会等名: 11th Int'l. Conf. on Concept Lattices and Their Applications (CLA 2014)
  • 発表場所: Kosice （Slovakia）
  • 年月日: 2014-10-10
• [学会発表] 分散関係データベースからの飽和パターンマイニングにおけるマージ演算の効率化 (2014)
  • 著者名/発表者名: 谷本 翔一, 神谷 洋平, 世木 博久
  • 学会等名: 情報処理学会・第76回全国大会
  • 発表場所: 東京都
• [学会発表] Extending Co-logic Programs for Branching-Time Model Checking (2013)
  • 著者名/発表者名: 世木 博久
  • 学会等名: 23rd International Symposium on Logic-Based Program Synthesis and Transformation
  • 発表場所: Madrid, Spain
• [学会発表] Proving Properties of Co-logic Programs with Negation by Program Transformations (2012)
  • 著者名/発表者名: 世木 博久
  • 学会等名: 22nd Int'l. Symp. on Logic-Based Program Synthesis and Transformation (LOPSTR2012)
  • 発表場所: Leuven, Belgium
• [学会発表] Distributed Closed Pattern Mining in Multi-Relational Data based on Iceberg Query Lattices: Some Preliminary Results (2012)
  • 著者名/発表者名: 世木 博久，谷本 翔一
  • 学会等名: 9th Int'l. Conf. on Concept Lattices and Their Applications (CLA 2012)
  • 発表場所: Fuengirola, Spain
• [図書] Pre-Proc. of 24th Int'l. Symp. on Logic-Based Program Synthesis and Transformation (LOPSTR2014) (2014)
  • 著者名/発表者名: M. Proietti, H. Seki
  • 総ページ数: 311
  • 出版者: Istituto Di Analisi Dei Sistemi Ed Informatica, CNR