Study on Software Verification Methods Using Program Transformation Handling Infinite Terms

2015 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

知能情報学