Study on Software Verification Methods Using Program Transformation Handling Infinite Terms

• Project/Area Number: 24500171
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Intelligent informatics
• Research Institution: Nagoya Institute of Technology
• Principal Investigator: Seki Hirohisa 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
• Project Period (FY): 2012-04-01 – 2016-03-31
• Project Status: Completed (Fiscal Year 2015)
• Budget Amount: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000); Fiscal Year 2014: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000); Fiscal Year 2013: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000); Fiscal Year 2012: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: 探索・論理・推論アルゴリズム / 計算論理 / プログラム推論 / プログラム変換 / システム検証

Outline of Final Research Achievements

The overall objective of this research is to develop a computational-logic based methodology for verifying software such as reactive systems using transformational verification methods; we use logic programs to represent a given system and reason about its properties. We have obtained the following three main results:
(1) We have proposed a reasoning method for co-logic programs. We have shown by some examples that it can be used for verifying some given specifications in a succinct way. (2) We have proposed an extended framework for co-logic programs, and shown that it is applicable to the model checking problem for CTL temporal logic formulas. (3) We have proposed a new method for pattern mining which will become a basis for specification discovery.

Research Products

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